src/Pure/Thy/thy_parse.ML
changeset 6352 d015ccae03da
parent 6328 dc72cf821659
child 6378 5780d71203bb
     1.1 --- a/src/Pure/Thy/thy_parse.ML	Thu Mar 11 21:52:32 1999 +0100
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Thu Mar 11 21:52:49 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, "IsarThy.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