--- 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;