src/Pure/ROOT.ML
changeset 1078 e57beb974dd7
parent 1072 0140ff702b23
child 1228 7d6b0241afab
     1.1 --- a/src/Pure/ROOT.ML	Fri Apr 28 11:52:43 1995 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Fri Apr 28 15:38:15 1995 +0200
     1.3 @@ -67,6 +67,23 @@
     1.4  structure Pure = struct val thy = pure_thy end;
     1.5  structure CPure = struct val thy = cpure_thy end;
     1.6  
     1.7 +(* hide functors; saves space in PolyML *)
     1.8 +functor SymtabFun() = struct end;
     1.9 +functor TypeFun() = struct end;
    1.10 +functor SignFun() = struct end;
    1.11 +functor SequenceFun() = struct end;
    1.12 +functor EnvirFun() = struct end;
    1.13 +functor PatternFun() = struct end;
    1.14 +functor UnifyFun() = struct end;
    1.15 +functor NetFun() = struct end;
    1.16 +functor LogicFun() = struct end;
    1.17 +functor ThmFun() = struct end;
    1.18 +functor DruleFun() = struct end;
    1.19 +functor TacticalFun() = struct end;
    1.20 +functor TacticFun() = struct end;
    1.21 +functor GoalsFun() = struct end;
    1.22 +functor AxClassFun() = struct end;
    1.23 +
    1.24  (*Theory parser and loader*)
    1.25  cd "Thy";
    1.26  use "ROOT.ML";