src/Pure/Thy/thy_parse.ML
changeset 2253 95b615550b8b
parent 2231 71385461570a
child 2360 1b6bc618c356
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Wed Nov 27 16:36:36 1996 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Wed Nov 27 16:40:23 1996 +0100
     1.3 @@ -486,7 +486,10 @@
     1.4          ^ postxt ^ "\n\
     1.5          \\n\
     1.6          \end;\n\
     1.7 -        \end;\n"
     1.8 +        \end;\n\
     1.9 +        \\n\
    1.10 +        \open " ^ thy_name ^ ";\n\
    1.11 +        \\n"
    1.12      | None =>
    1.13          "val thy = " ^ old_thys ^ " false;\n\
    1.14          \\n\
    1.15 @@ -497,7 +500,11 @@
    1.16          \\n\
    1.17          \val _ = store_theory (thy, " ^ quote thy_name ^ ");\n\
    1.18          \\n\
    1.19 -        \end;\n");
    1.20 +        \end;\n\
    1.21 +        \\n\
    1.22 +        \open " ^ thy_name ^ ";\n\
    1.23 +        \\n");
    1.24 +
    1.25  
    1.26  fun theory_defn sectab tname =
    1.27    header -- optional (extension sectab >> Some) None -- eof