IsarThy.begin/end_theory;
authorwenzelm
Tue Mar 09 12:18:02 1999 +0100 (1999-03-09)
changeset 6328dc72cf821659
parent 6327 c6abb5884fed
child 6329 bbd03b119f36
IsarThy.begin/end_theory;
src/Pure/Thy/thy_parse.ML
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Tue Mar 09 12:17:40 1999 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Tue Mar 09 12:18:02 1999 +0100
     1.3 @@ -464,7 +464,7 @@
     1.4  (* header *)
     1.5  
     1.6  fun mk_header (thy_name, parents) =
     1.7 -  (thy_name, "ThyInfo.begin_theory " ^ cat (quote thy_name) (mk_list parents));
     1.8 +  (thy_name, "IsarThy.begin_theory " ^ cat (quote thy_name) (mk_list parents) ^ "[]");
     1.9  
    1.10  val header = ident --$$ "=" -- enum1 "+" name >> mk_header;
    1.11  
    1.12 @@ -514,7 +514,7 @@
    1.13    \\n"
    1.14    ^ extxt ^ "\n\
    1.15    \\n\
    1.16 -  \|> ThyInfo.end_theory;\n\
    1.17 +  \|> IsarThy.end_theory;\n\
    1.18    \\n\
    1.19    \val _ = context thy;\n\
    1.20    \\n\