src/Pure/Thy/thy_parse.ML

 
 
 (* 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;
 
 
 (* extension *)

   \|> Theory.add_trfunsT typed_print_translation\n\
   \|> Theory.add_tokentrfuns token_translation\n\
   \\n"
   ^ extxt ^ "\n\
   \\n\
-  \|> ThyInfo.end_theory;\n\
+  \|> IsarThy.end_theory;\n\
   \\n\
   \val _ = context thy;\n\
   \\n\
   \\n"
   ^ postxt ^ "\n\