src/Pure/Isar/named_target.ML
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