# HG changeset patch
# User wenzelm
# Date 1138913995 -3600
# Node ID 5a476b10d69c15e878a97a5fd072c609abfb40a5
# Parent  57f19fad8c2a9228baf39744b541b1e502665363
do not open structure;

diff -r 57f19fad8c2a -r 5a476b10d69c src/FOL/FOL.ML
--- a/src/FOL/FOL.ML	Thu Feb 02 19:57:13 2006 +0100
+++ b/src/FOL/FOL.ML	Thu Feb 02 21:59:55 2006 +0100
@@ -4,5 +4,3 @@
   val thy = the_context ();
   val classical = classical;
 end;
-
-open FOL;
diff -r 57f19fad8c2a -r 5a476b10d69c src/FOL/IFOL.ML
--- a/src/FOL/IFOL.ML	Thu Feb 02 19:57:13 2006 +0100
+++ b/src/FOL/IFOL.ML	Thu Feb 02 21:59:55 2006 +0100
@@ -24,5 +24,3 @@
   val eq_reflection = eq_reflection;
   val iff_reflection = iff_reflection;
 end;
-
-open IFOL;