# HG changeset patch
# User wenzelm
# Date 849109223 -3600
# Node ID 95b615550b8b45a775989cbddaebb608d4c8a6bd
# Parent  d54af138f7b2275e2309d60ad61eca68d1e61f8d
use_thy now automatically opens theory structures;

diff -r d54af138f7b2 -r 95b615550b8b src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Wed Nov 27 16:36:36 1996 +0100
+++ b/src/Pure/Thy/thy_parse.ML	Wed Nov 27 16:40:23 1996 +0100
@@ -486,7 +486,10 @@
         ^ postxt ^ "\n\
         \\n\
         \end;\n\
-        \end;\n"
+        \end;\n\
+        \\n\
+        \open " ^ thy_name ^ ";\n\
+        \\n"
     | None =>
         "val thy = " ^ old_thys ^ " false;\n\
         \\n\
@@ -497,7 +500,11 @@
         \\n\
         \val _ = store_theory (thy, " ^ quote thy_name ^ ");\n\
         \\n\
-        \end;\n");
+        \end;\n\
+        \\n\
+        \open " ^ thy_name ^ ";\n\
+        \\n");
+
 
 fun theory_defn sectab tname =
   header -- optional (extension sectab >> Some) None -- eof