1.1 --- a/src/Pure/Isar/toplevel.ML	Sat Jun 07 08:16:03 2014 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Jun 07 08:16:03 2014 +0200
     1.3 @@ -103,18 +103,20 @@
     1.4  exception UNDEF = Runtime.UNDEF;
     1.5  
     1.6  
     1.7 -(* local theory wrappers *)
     1.8 +(* named target wrappers *)
     1.9  
    1.10 -val loc_init = Named_Target.context_cmd;
    1.11 -val loc_exit = Local_Theory.assert_bottom true #> Local_Theory.exit_global;
    1.12 +val named_init = Named_Target.context_cmd;
    1.13 +val named_exit = Local_Theory.assert_bottom true #> Local_Theory.exit_global;
    1.14  
    1.15 -fun loc_begin loc (Context.Theory thy) =
    1.16 -      (Context.Theory o loc_exit, loc_init (the_default ("-", Position.none) loc) thy)
    1.17 -  | loc_begin NONE (Context.Proof lthy) =
    1.18 +fun named_begin NONE (Context.Theory thy) =
    1.19 +      (Context.Theory o named_exit, named_init ("-", Position.none) thy)
    1.20 +  | named_begin (SOME loc) (Context.Theory thy) =
    1.21 +      (Context.Theory o named_exit, named_init loc thy)
    1.22 +  | named_begin NONE (Context.Proof lthy) =
    1.23        (Context.Proof o Local_Theory.restore, lthy)
    1.24 -  | loc_begin (SOME loc) (Context.Proof lthy) =
    1.25 +  | named_begin (SOME loc) (Context.Proof lthy) =
    1.26        (Context.Proof o Named_Target.reinit lthy,
    1.27 -        loc_init loc (loc_exit (Local_Theory.assert_nonbrittle lthy)));
    1.28 +        named_init loc (named_exit (Local_Theory.assert_nonbrittle lthy)));
    1.29  
    1.30  
    1.31  (* datatype node *)
    1.32 @@ -411,7 +413,7 @@
    1.33    (fn Theory (Context.Theory thy, _) =>
    1.34          let
    1.35            val lthy = f thy;
    1.36 -          val gthy = if begin then Context.Proof lthy else Context.Theory (loc_exit lthy);
    1.37 +          val gthy = if begin then Context.Proof lthy else Context.Theory (named_exit lthy);
    1.38            val _ =
    1.39              if begin then
    1.40                Pretty.writeln (Pretty.mark Markup.state (Pretty.chunks (Local_Theory.pretty lthy)))
    1.41 @@ -420,7 +422,7 @@
    1.42      | _ => raise UNDEF));
    1.43  
    1.44  val end_local_theory = transaction (fn _ =>
    1.45 -  (fn Theory (Context.Proof lthy, _) => Theory (Context.Theory (loc_exit lthy), SOME lthy)
    1.46 +  (fn Theory (Context.Proof lthy, _) => Theory (Context.Theory (named_exit lthy), SOME lthy)
    1.47      | _ => raise UNDEF));
    1.48  
    1.49  fun open_target f = transaction (fn _ =>
    1.50 @@ -448,7 +450,7 @@
    1.51  fun local_theory_presentation loc f = present_transaction (fn int =>
    1.52    (fn Theory (gthy, _) =>
    1.53          let
    1.54 -          val (finish, lthy) = loc_begin loc gthy;
    1.55 +          val (finish, lthy) = named_begin loc gthy;
    1.56            val lthy' = lthy
    1.57              |> Local_Theory.new_group
    1.58              |> f int
    1.59 @@ -504,7 +506,7 @@
    1.60  
    1.61  fun local_theory_to_proof' loc f = begin_proof
    1.62    (fn int => fn gthy =>
    1.63 -    let val (finish, lthy) = loc_begin loc gthy
    1.64 +    let val (finish, lthy) = named_begin loc gthy
    1.65      in (finish o Local_Theory.reset_group, f int (Local_Theory.new_group lthy)) end);
    1.66  
    1.67  fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f);