changeset 47946 | 451fc10a81f3 |
parent 47943 | 8a6124d09ff5 |
child 47956 | bfad2f674d0e |
1.1 --- a/src/Pure/Isar/named_target.ML Wed Mar 21 21:24:13 2012 +0100 1.2 +++ b/src/Pure/Isar/named_target.ML Wed Mar 21 23:26:35 2012 +0100 1.3 @@ -215,7 +215,7 @@ 1.4 val theory_init = init I ""; 1.5 1.6 val reinit = 1.7 - assert #> Data.get #> the #> 1.8 + Local_Theory.assert_bottom true #> Data.get #> the #> 1.9 (fn Target {target, before_exit, ...} => Local_Theory.exit_global #> init before_exit target); 1.10 1.11 fun context_cmd ("-", _) thy = init I "" thy