use_thy now automatically opens theory structures;

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