Let Holmake's internal_functions structure depend on Holmake_tools

HOL-Theorem-Prover · Aug 11, 2022 · f72dd5a · f72dd5a
1 parent 917d17c
commit f72dd5a
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 6 deletions.
diff --git a/tools/Holmake/hmcore.ML b/tools/Holmake/hmcore.ML
@@ -19,12 +19,12 @@ val _ = let
 in
   app (myuse hmakedir) ["HOLFS_dtype.sml", "HFS_NameMunge.sig"];
   myuse (OS.Path.concat(hmakedir, "poly")) "HFS_NameMunge.sml";
-  app appthis ["HOLFileSys", "regexpMatch", "parse_glob", "internal_functions",
+  app appthis ["HOLFileSys", "regexpMatch", "parse_glob",
                "Holdep_tokens"] ;
   app (myuse hmakedir) ["QuoteFilter.sml", "Holmake_tools_dtype.sml",
                         "terminal_primitives.sig",
                         "poly-terminal-prims.ML"];
-  app appthis ["QFRead", "Holdep", "Holmake_tools",
+  app appthis ["QFRead", "Holdep", "Holmake_tools", "internal_functions",
                "Holmake_types",
                "ReadHMF"]
 end;
diff --git a/tools/Holmake/hmcore.mlb b/tools/Holmake/hmcore.mlb
@@ -22,15 +22,15 @@ regexpMatch.sig
 regexpMatch.sml
 parse_glob.sig
 parse_glob.sml
-internal_functions.sig
-internal_functions.sml
 tailbuffer.sig
 tailbuffer.sml
 Holmake_tools_dtype.sml
 terminal_primitives.sig
 poly-terminal-prims.ML
 Holmake_tools.sig
 Holmake_tools.sml
+internal_functions.sig
+internal_functions.sml
 Holmake_types.sig
 Holmake_types.sml
 ReadHMF.sig

diff --git a/tools/configure.sml b/tools/configure.sml
@@ -319,8 +319,6 @@ val _ =
     FileSys.chDir "..";
     compile [] "HOLFileSys.sig";
     compile [] "HOLFileSys.sml";
-    compile [] "internal_functions.sig";
-    compile [] "internal_functions.sml";
     compile [] "Holdep_tokens.sig";
     compile [] "Holdep_tokens.sml";
     compile [] "QuoteFilter.sml";
@@ -333,6 +331,8 @@ val _ =
     compile ["-I", "mosml"] "Holdep.sml";
     compile [] "Holmake_tools.sig";
     compile [] "Holmake_tools.sml";
+    compile [] "internal_functions.sig";
+    compile [] "internal_functions.sml";
     compile [] "Holmake_types.sig";
     compile [] "Holmake_types.sml";
     compile [] "ReadHMF.sig";