changeset 47274 | feef9b0b6031 |
parent 47251 | 13a770bd5544 |
child 47275 | fc95b8b6c260 |
--- a/src/Pure/Isar/named_target.ML Mon Apr 02 17:00:32 2012 +0200 +++ b/src/Pure/Isar/named_target.ML Mon Apr 02 19:10:52 2012 +0200 @@ -192,7 +192,7 @@ Local_Theory.assert_bottom true #> Data.get #> the #> (fn Target {target, before_exit, ...} => Local_Theory.exit_global #> init before_exit target); -fun context_cmd ("-", _) thy = init I "" thy +fun context_cmd ("-", _) thy = theory_init thy | context_cmd target thy = init I (Locale.check thy target) thy; end;