# HG changeset patch
# User wenzelm
# Date 920978282 -3600
# Node ID dc72cf8216593aacc35c42265e52135581c02ec9
# Parent  c6abb5884fed7040ba2ce949fcda48b2cfd3f1f0
IsarThy.begin/end_theory;

diff -r c6abb5884fed -r dc72cf821659 src/Pure/Thy/thy_parse.ML
--- 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\