--- 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";