# HG changeset patch
# User wenzelm
# Date 769963906 -7200
# Node ID 4c66b15777534cf859c91902ebb79d498f84835a
# Parent  16a8fe4f22503759839a629ddc497dbe25884686
added "axclass.ML", structure AxClass;

diff -r 16a8fe4f2250 -r 4c66b1577753 src/Pure/ROOT.ML
--- 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;