| changeset 17367 | 44518c82100a |
| parent 17285 | 1fe83f912bd6 |
| child 17412 | e26cb20ef0cc |
--- a/src/Pure/Thy/thy_parse.ML Tue Sep 13 22:19:51 2005 +0200 +++ b/src/Pure/Thy/thy_parse.ML Tue Sep 13 22:19:52 2005 +0200 @@ -453,7 +453,7 @@ (* header *) fun mk_header (thy_name, parents) = - (thy_name, "IsarThy.begin_theory " ^ cat (Library.quote thy_name) (mk_list parents) ^ " []"); + (thy_name, "IsarThy.begin_theory " ^ cat (Library.quote thy_name) (mk_list parents) ^ " [] false"); val header = ident --$$ "=" -- enum1 "+" name >> mk_header;