Remove more bare expressions for mosml's sake

build -t still doesn't work under Moscow ML because of issues trying to compile regular-play/emit
HOL-Theorem-Prover · Nov 8, 2023 · 0d380a5 · 0d380a5
1 parent ee74295
commit 0d380a5
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 6 deletions.
diff --git a/examples/formal-languages/lambek/CutFreeScript.sml b/examples/formal-languages/lambek/CutFreeScript.sml
@@ -44,7 +44,7 @@ end;
 
 val _ = new_theory "CutFree";
 
-hide "S";
+val _ = hide "S";
 
 (*** Module: CutSequent ***)
 

diff --git a/examples/formal-languages/regular/regular-play/emit/emit_regexScript.sml b/examples/formal-languages/regular/regular-play/emit/emit_regexScript.sml
@@ -68,11 +68,7 @@ fun copyDep name =
 
 
 
-copyDep "combin";
-copyDep "pair";
-copyDep "num";
-copyDep "list";
-copyDep "rich_list";
+val _ = List.app copyDep ["combin","pair" ,"num" ,"list" ,"rich_list"]