src/Pure/ROOT.ML
changeset 1498 7b7d20e89b1b
parent 1443 ff8a804e0201
child 1528 608dd813b437
--- a/src/Pure/ROOT.ML	Thu Feb 15 10:51:22 1996 +0100
+++ b/src/Pure/ROOT.ML	Fri Feb 16 11:35:52 1996 +0100
@@ -40,47 +40,9 @@
 use "goals.ML";
 use "axclass.ML";
 
-(*Will be visible to all object-logics.*)
-structure Type = TypeFun(structure Symtab=Symtab and Syntax=Syntax);
-structure Sign = SignFun(structure Type=Type and Syntax=Syntax);
-structure Sequence = SequenceFun();
-structure Envir = EnvirFun();
-structure Pattern = PatternFun(structure Sign=Sign and Envir=Envir);
-structure Unify = UnifyFun(structure Sign=Sign and Envir=Envir
-                           and Sequence=Sequence and Pattern=Pattern);
-structure Net = NetFun();
-structure Logic = LogicFun(structure Unify=Unify and Net=Net);
-structure Thm = ThmFun(structure Logic=Logic and Unify=Unify and Net=Net
-                             and Pattern=Pattern);
-structure Drule = DruleFun(structure Logic=Logic and Thm=Thm);
-structure Tactical = TacticalFun(structure Logic=Logic and Drule=Drule);
-structure Tactic = TacticFun(structure Logic=Logic and Drule=Drule
-                             and Tactical=Tactical and Net=Net);
-structure Goals = GoalsFun(structure Logic=Logic and Drule=Drule
-                           and Tactic=Tactic and Pattern=Pattern);
-structure AxClass = AxClassFun(structure Logic = Logic
-  and Goals = Goals and Tactic = Tactic);
-open BasicSyntax Thm Drule Tactical Tactic Goals;
-
 structure Pure = struct val thy = pure_thy end;
 structure CPure = struct val thy = cpure_thy end;
 
-(* hide functors; saves space in PolyML *)
-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";