# HG changeset patch
# User wenzelm
# Date 1126642792 -7200
# Node ID 44518c82100afa3eede3e72cda1595c93e2def1c
# Parent  325707c676e225a769ae63f686addebd32d754b3
IsarThy.begin_theory;

diff -r 325707c676e2 -r 44518c82100a src/Pure/Thy/thy_parse.ML
--- 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;