# HG changeset patch
# User wenzelm
# Date 781975750 -3600
# Node ID 034fda1c48739826b245f2382e7254beca5a2e1f
# Parent  8a5f6961250f34a98257a50caddeb76dc0e746b9
AxClass no longer open;

diff -r 8a5f6961250f -r 034fda1c4873 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Oct 12 12:20:18 1994 +0100
+++ b/src/Pure/ROOT.ML	Wed Oct 12 16:29:10 1994 +0100
@@ -62,7 +62,7 @@
                            and Tactic=Tactic and Pattern=Pattern);
 structure AxClass = AxClassFun(structure Logic = Logic
   and Goals = Goals and Tactic = Tactic);
-open BasicSyntax Thm Drule Tactical Tactic Goals AxClass;
+open BasicSyntax Thm Drule Tactical Tactic Goals;
 
 structure Pure = struct val thy = pure_thy end;