src/Pure/Thy/ROOT.ML

--- a/src/Pure/Thy/ROOT.ML	Fri Apr 28 11:52:43 1995 +0200
+++ b/src/Pure/Thy/ROOT.ML	Fri Apr 28 15:38:15 1995 +0200
@@ -13,6 +13,10 @@
 structure ThyParse = ThyParseFun(structure Symtab = Symtab
   and ThyScan = ThyScan);
 
+(* hide functors; saves space in PolyML *)
+functor ThyScanFun() = struct end;
+functor ThyParseFun() = struct end;
+
 use "thy_syn.ML";
 use "thy_read.ML";
 
@@ -20,6 +24,8 @@
 structure Readthy = ReadthyFUN(structure ThySyn = ThySyn);
 open Readthy;
 
+(* Do not hide ThySynFun and ReadthyFUN; they are still used *)
+
 fun init_thy_reader () =
   use_string
    ["structure Readthy = ReadthyFUN(structure ThySyn = ThySyn);",