src/Pure/Isar/toplevel.ML

--- a/src/Pure/Isar/toplevel.ML	Sat Jun 07 08:16:03 2014 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sat Jun 07 08:16:03 2014 +0200
@@ -103,18 +103,20 @@
 exception UNDEF = Runtime.UNDEF;
 
 
-(* local theory wrappers *)
+(* named target wrappers *)
 
-val loc_init = Named_Target.context_cmd;
-val loc_exit = Local_Theory.assert_bottom true #> Local_Theory.exit_global;
+val named_init = Named_Target.context_cmd;
+val named_exit = Local_Theory.assert_bottom true #> Local_Theory.exit_global;
 
-fun loc_begin loc (Context.Theory thy) =
-      (Context.Theory o loc_exit, loc_init (the_default ("-", Position.none) loc) thy)
-  | loc_begin NONE (Context.Proof lthy) =
+fun named_begin NONE (Context.Theory thy) =
+      (Context.Theory o named_exit, named_init ("-", Position.none) thy)
+  | named_begin (SOME loc) (Context.Theory thy) =
+      (Context.Theory o named_exit, named_init loc thy)
+  | named_begin NONE (Context.Proof lthy) =
       (Context.Proof o Local_Theory.restore, lthy)
-  | loc_begin (SOME loc) (Context.Proof lthy) =
+  | named_begin (SOME loc) (Context.Proof lthy) =
       (Context.Proof o Named_Target.reinit lthy,
-        loc_init loc (loc_exit (Local_Theory.assert_nonbrittle lthy)));
+        named_init loc (named_exit (Local_Theory.assert_nonbrittle lthy)));
 
 
 (* datatype node *)
@@ -411,7 +413,7 @@
   (fn Theory (Context.Theory thy, _) =>
         let
           val lthy = f thy;
-          val gthy = if begin then Context.Proof lthy else Context.Theory (loc_exit lthy);
+          val gthy = if begin then Context.Proof lthy else Context.Theory (named_exit lthy);
           val _ =
             if begin then
               Pretty.writeln (Pretty.mark Markup.state (Pretty.chunks (Local_Theory.pretty lthy)))
@@ -420,7 +422,7 @@
     | _ => raise UNDEF));
 
 val end_local_theory = transaction (fn _ =>
-  (fn Theory (Context.Proof lthy, _) => Theory (Context.Theory (loc_exit lthy), SOME lthy)
+  (fn Theory (Context.Proof lthy, _) => Theory (Context.Theory (named_exit lthy), SOME lthy)
     | _ => raise UNDEF));
 
 fun open_target f = transaction (fn _ =>
@@ -448,7 +450,7 @@
 fun local_theory_presentation loc f = present_transaction (fn int =>
   (fn Theory (gthy, _) =>
         let
-          val (finish, lthy) = loc_begin loc gthy;
+          val (finish, lthy) = named_begin loc gthy;
           val lthy' = lthy
             |> Local_Theory.new_group
             |> f int
@@ -504,7 +506,7 @@
 
 fun local_theory_to_proof' loc f = begin_proof
   (fn int => fn gthy =>
-    let val (finish, lthy) = loc_begin loc gthy
+    let val (finish, lthy) = named_begin loc gthy
     in (finish o Local_Theory.reset_group, f int (Local_Theory.new_group lthy)) end);
 
 fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f);