| changeset 47069 | 451fc10a81f3 |
| parent 47066 | 8a6124d09ff5 |
| child 47080 | bfad2f674d0e |
--- a/src/Pure/Isar/named_target.ML Wed Mar 21 21:24:13 2012 +0100 +++ b/src/Pure/Isar/named_target.ML Wed Mar 21 23:26:35 2012 +0100 @@ -215,7 +215,7 @@ val theory_init = init I ""; val reinit = - assert #> Data.get #> the #> + 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