src/Pure/ROOT.ML
changeset 403 4c66b1577753
parent 83 de9316670e89
child 607 72fc777dbda0
     1.1 --- a/src/Pure/ROOT.ML	Thu May 26 16:45:56 1994 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Thu May 26 16:51:46 1994 +0200
     1.3 @@ -40,6 +40,7 @@
     1.4  use "tctical.ML";
     1.5  use "tactic.ML";
     1.6  use "goals.ML";
     1.7 +use "axclass.ML";
     1.8  
     1.9  (*Will be visible to all object-logics.*)
    1.10  structure Type = TypeFun(structure Symtab=Symtab and Syntax=Syntax);
    1.11 @@ -59,7 +60,9 @@
    1.12                               and Tactical=Tactical and Net=Net);
    1.13  structure Goals = GoalsFun(structure Logic=Logic and Drule=Drule
    1.14                             and Tactic=Tactic and Pattern=Pattern);
    1.15 -open BasicSyntax Thm Drule Tactical Tactic Goals;
    1.16 +structure AxClass = AxClassFun(structure Logic = Logic 
    1.17 +  and Goals = Goals and Tactic = Tactic);
    1.18 +open BasicSyntax Thm Drule Tactical Tactic Goals AxClass;
    1.19  
    1.20  structure Pure = struct val thy = pure_thy end;
    1.21