avoid arcane Local_Theory.reinit entirely
authorhaftmann
Wed Aug 11 17:16:02 2010 +0200 (2010-08-11 ago)
changeset 38380cf42d8355844
parent 38379 67d71449e85b
child 38381 7d1e2a6831ec
avoid arcane Local_Theory.reinit entirely
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Aug 11 16:02:03 2010 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Aug 11 17:16:02 2010 +0200
     1.3 @@ -112,8 +112,10 @@
     1.4  
     1.5  fun loc_finish _ (Context.Theory _) = Context.Theory o loc_exit
     1.6    | loc_finish NONE (Context.Proof _) = Context.Proof o Local_Theory.restore
     1.7 -  | loc_finish (SOME _) (Context.Proof lthy) = fn lthy' =>
     1.8 -      Context.Proof (Local_Theory.reinit (Local_Theory.raw_theory (K (loc_exit lthy')) lthy));
     1.9 +  | loc_finish (SOME _) (Context.Proof lthy) = fn lthy' => let
    1.10 +        val target_name = #target (Named_Target.peek lthy);
    1.11 +        val target = if target_name = "" then NONE else SOME target_name;
    1.12 +      in Context.Proof (Named_Target.init target (loc_exit lthy')) end;
    1.13  
    1.14  
    1.15  (* datatype node *)