author | wenzelm |
Thu, 11 Mar 1999 21:52:49 +0100 | |
changeset 6352 | d015ccae03da |
parent 6351 | 74763258b78b |
child 6353 | 5a76eb9030df |
--- a/src/Pure/Thy/thy_parse.ML Thu Mar 11 21:52:32 1999 +0100 +++ b/src/Pure/Thy/thy_parse.ML Thu Mar 11 21:52:49 1999 +0100 @@ -464,7 +464,7 @@ (* header *) fun mk_header (thy_name, parents) = - (thy_name, "IsarThy.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;