src/Pure/ROOT.ML
changeset 1078 e57beb974dd7
parent 1072 0140ff702b23
child 1228 7d6b0241afab
--- 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";