src/Pure/Isar/toplevel.ML
changeset 59032 f36496364ce1
parent 59000 ed09ae4ea2d8
child 59055 5a7157b8e870
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sat Nov 22 14:57:04 2014 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Nov 22 15:27:48 2014 +0100
     1.3 @@ -415,10 +415,7 @@
     1.4          | NONE => raise UNDEF)
     1.5      | _ => raise UNDEF));
     1.6  
     1.7 -
     1.8 -local
     1.9 -
    1.10 -fun local_theory_presentation loc f = present_transaction (fn int =>
    1.11 +fun local_theory' loc f = present_transaction (fn int =>
    1.12    (fn Theory (gthy, _) =>
    1.13          let
    1.14            val (finish, lthy) = Named_Target.switch loc gthy;
    1.15 @@ -427,15 +424,16 @@
    1.16              |> f int
    1.17              |> Local_Theory.reset_group;
    1.18          in Theory (finish lthy', SOME lthy') end
    1.19 -    | _ => raise UNDEF));
    1.20 +    | _ => raise UNDEF))
    1.21 +  (K ());
    1.22  
    1.23 -in
    1.24 +fun local_theory loc f = local_theory' loc (K f);
    1.25  
    1.26 -fun local_theory' loc f = local_theory_presentation loc f (K ());
    1.27 -fun local_theory loc f = local_theory' loc (K f);
    1.28 -fun present_local_theory loc = local_theory_presentation loc (K I);
    1.29 -
    1.30 -end;
    1.31 +fun present_local_theory loc = present_transaction (fn int =>
    1.32 +  (fn Theory (gthy, _) =>
    1.33 +        let val (finish, lthy) = Named_Target.switch loc gthy;
    1.34 +        in Theory (finish lthy, SOME lthy) end
    1.35 +    | _ => raise UNDEF));
    1.36  
    1.37  
    1.38  (* proof transitions *)