src/Pure/ROOT.ML
changeset 403 4c66b1577753
parent 83 de9316670e89
child 607 72fc777dbda0
--- a/src/Pure/ROOT.ML	Thu May 26 16:45:56 1994 +0200
+++ b/src/Pure/ROOT.ML	Thu May 26 16:51:46 1994 +0200
@@ -40,6 +40,7 @@
 use "tctical.ML";
 use "tactic.ML";
 use "goals.ML";
+use "axclass.ML";
 
 (*Will be visible to all object-logics.*)
 structure Type = TypeFun(structure Symtab=Symtab and Syntax=Syntax);
@@ -59,7 +60,9 @@
                              and Tactical=Tactical and Net=Net);
 structure Goals = GoalsFun(structure Logic=Logic and Drule=Drule
                            and Tactic=Tactic and Pattern=Pattern);
-open BasicSyntax Thm Drule Tactical Tactic Goals;
+structure AxClass = AxClassFun(structure Logic = Logic 
+  and Goals = Goals and Tactic = Tactic);
+open BasicSyntax Thm Drule Tactical Tactic Goals AxClass;
 
 structure Pure = struct val thy = pure_thy end;