author | wenzelm |
Thu, 14 Dec 2006 15:31:20 +0100 | |
changeset 21843 | 2015be1b6a03 |
parent 21842 | 3d8ab6545049 |
child 21844 | e10b8bd7a886 |
--- a/src/Pure/Isar/isar_syn.ML Thu Dec 14 01:19:27 2006 +0100 +++ b/src/Pure/Isar/isar_syn.ML Thu Dec 14 15:31:20 2006 +0100 @@ -371,7 +371,7 @@ -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, []) -- P.opt_begin >> (fn (((is_open, name), (expr, elems)), begin) => - Toplevel.begin_local_theory begin + (begin ? Toplevel.print) o Toplevel.begin_local_theory begin (Locale.add_locale is_open name expr elems #-> TheoryTarget.begin false))); val interpretationP =