--- a/src/Pure/Thy/thy_parse.ML Tue Mar 09 12:17:40 1999 +0100
+++ b/src/Pure/Thy/thy_parse.ML Tue Mar 09 12:18:02 1999 +0100
@@ -464,7 +464,7 @@
(* header *)
fun mk_header (thy_name, parents) =
- (thy_name, "ThyInfo.begin_theory " ^ cat (quote thy_name) (mk_list parents));
+ (thy_name, "IsarThy.begin_theory " ^ cat (quote thy_name) (mk_list parents) ^ "[]");
val header = ident --$$ "=" -- enum1 "+" name >> mk_header;
@@ -514,7 +514,7 @@
\\n"
^ extxt ^ "\n\
\\n\
- \|> ThyInfo.end_theory;\n\
+ \|> IsarThy.end_theory;\n\
\\n\
\val _ = context thy;\n\
\\n\