# HG changeset patch
# User haftmann
# Date 1404281029 -7200
# Node ID cc309f3c04906aee207674a64b3ea860953732c5
# Parent  950dc744645450adb3cf46cfa0c1ec1d24194f01
restore exactly named target, prevent non-named targets to participate in the ad-hoc switch game

diff -r 950dc7446454 -r cc309f3c0490 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Wed Jul 02 08:03:48 2014 +0200
+++ b/src/Pure/Isar/named_target.ML	Wed Jul 02 08:03:49 2014 +0200
@@ -42,6 +42,11 @@
     SOME ("", _) => true
   | _ => false;
 
+fun target_of lthy =
+  case get_data lthy of
+    NONE => error "Not in a named target"
+  | SOME (target, _) => target;
+
 fun locale_name_of NONE = NONE
   | locale_name_of (SOME ("", _)) = NONE
   | locale_name_of (SOME (locale, _)) = SOME locale;
@@ -182,7 +187,7 @@
   | switch NONE (Context.Proof lthy) =
       (Context.Proof o Local_Theory.restore, lthy)
   | switch (SOME name) (Context.Proof lthy) =
-      (Context.Proof o init (the (locale_of lthy)) o exit,
+      (Context.Proof o init (target_of lthy) o exit,
         (begin name o exit o Local_Theory.assert_nonbrittle) lthy);
 
 end;