# HG changeset patch
# User nipkow
# Date 799076295 -7200
# Node ID e57beb974dd77d7a384aedfdb51c8ec98447876b
# Parent  c2df11ae8b551c78bf1b0c033613a5181061d487
Added

functor f() = struct end

to hide functors to save space.

diff -r c2df11ae8b55 -r e57beb974dd7 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Apr 28 11:52:43 1995 +0200
+++ b/src/Pure/ROOT.ML	Fri Apr 28 15:38:15 1995 +0200
@@ -67,6 +67,23 @@
 structure Pure = struct val thy = pure_thy end;
 structure CPure = struct val thy = cpure_thy end;
 
+(* hide functors; saves space in PolyML *)
+functor SymtabFun() = struct end;
+functor TypeFun() = struct end;
+functor SignFun() = struct end;
+functor SequenceFun() = struct end;
+functor EnvirFun() = struct end;
+functor PatternFun() = struct end;
+functor UnifyFun() = struct end;
+functor NetFun() = struct end;
+functor LogicFun() = struct end;
+functor ThmFun() = struct end;
+functor DruleFun() = struct end;
+functor TacticalFun() = struct end;
+functor TacticFun() = struct end;
+functor GoalsFun() = struct end;
+functor AxClassFun() = struct end;
+
 (*Theory parser and loader*)
 cd "Thy";
 use "ROOT.ML";
diff -r c2df11ae8b55 -r e57beb974dd7 src/Pure/Syntax/ROOT.ML
--- a/src/Pure/Syntax/ROOT.ML	Fri Apr 28 11:52:43 1995 +0200
+++ b/src/Pure/Syntax/ROOT.ML	Fri Apr 28 15:38:15 1995 +0200
@@ -41,3 +41,14 @@
 structure Syntax = PrivateSyntax.Syntax;
 structure BasicSyntax = PrivateSyntax.BasicSyntax;
 
+(* hide functors; saves space in PolyML *)
+functor PrettyFun() = struct end;
+functor LexiconFun() = struct end;
+functor AstFun() = struct end;
+functor SynExtFun() = struct end;
+functor ParserFun() = struct end;
+functor TypeExtFun() = struct end;
+functor SynTransFun() = struct end;
+functor MixfixFun() = struct end;
+functor PrinterFun() = struct end;
+functor SyntaxFun() = struct end;
diff -r c2df11ae8b55 -r e57beb974dd7 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);",