src/Pure/ROOT.ML
changeset 1498 7b7d20e89b1b
parent 1443 ff8a804e0201
child 1528 608dd813b437
     1.1 --- a/src/Pure/ROOT.ML	Thu Feb 15 10:51:22 1996 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Fri Feb 16 11:35:52 1996 +0100
     1.3 @@ -40,47 +40,9 @@
     1.4  use "goals.ML";
     1.5  use "axclass.ML";
     1.6  
     1.7 -(*Will be visible to all object-logics.*)
     1.8 -structure Type = TypeFun(structure Symtab=Symtab and Syntax=Syntax);
     1.9 -structure Sign = SignFun(structure Type=Type and Syntax=Syntax);
    1.10 -structure Sequence = SequenceFun();
    1.11 -structure Envir = EnvirFun();
    1.12 -structure Pattern = PatternFun(structure Sign=Sign and Envir=Envir);
    1.13 -structure Unify = UnifyFun(structure Sign=Sign and Envir=Envir
    1.14 -                           and Sequence=Sequence and Pattern=Pattern);
    1.15 -structure Net = NetFun();
    1.16 -structure Logic = LogicFun(structure Unify=Unify and Net=Net);
    1.17 -structure Thm = ThmFun(structure Logic=Logic and Unify=Unify and Net=Net
    1.18 -                             and Pattern=Pattern);
    1.19 -structure Drule = DruleFun(structure Logic=Logic and Thm=Thm);
    1.20 -structure Tactical = TacticalFun(structure Logic=Logic and Drule=Drule);
    1.21 -structure Tactic = TacticFun(structure Logic=Logic and Drule=Drule
    1.22 -                             and Tactical=Tactical and Net=Net);
    1.23 -structure Goals = GoalsFun(structure Logic=Logic and Drule=Drule
    1.24 -                           and Tactic=Tactic and Pattern=Pattern);
    1.25 -structure AxClass = AxClassFun(structure Logic = Logic
    1.26 -  and Goals = Goals and Tactic = Tactic);
    1.27 -open BasicSyntax Thm Drule Tactical Tactic Goals;
    1.28 -
    1.29  structure Pure = struct val thy = pure_thy end;
    1.30  structure CPure = struct val thy = cpure_thy end;
    1.31  
    1.32 -(* hide functors; saves space in PolyML *)
    1.33 -functor TypeFun() = struct end;
    1.34 -functor SignFun() = struct end;
    1.35 -functor SequenceFun() = struct end;
    1.36 -functor EnvirFun() = struct end;
    1.37 -functor PatternFun() = struct end;
    1.38 -functor UnifyFun() = struct end;
    1.39 -functor NetFun() = struct end;
    1.40 -functor LogicFun() = struct end;
    1.41 -functor ThmFun() = struct end;
    1.42 -functor DruleFun() = struct end;
    1.43 -functor TacticalFun() = struct end;
    1.44 -functor TacticFun() = struct end;
    1.45 -functor GoalsFun() = struct end;
    1.46 -functor AxClassFun() = struct end;
    1.47 -
    1.48  (*Theory parser and loader*)
    1.49  cd "Thy";
    1.50  use "ROOT.ML";