sharpened criterion: bare named target is only at the bottom level

--- a/src/Pure/Isar/named_target.ML	Thu Jun 05 19:39:35 2014 +0200
+++ b/src/Pure/Isar/named_target.ML	Thu Jun 05 19:39:38 2014 +0200
@@ -40,12 +40,13 @@
   fun init _ = NONE;
 );
 
-val peek =
-  Data.get #> Option.map (fn Target {target, is_locale, is_class, ...} =>
-    {target = target, is_locale = is_locale, is_class = is_class});
+fun peek lthy =
+  if Local_Theory.level lthy = 1
+  then Option.map (fn Target {target, is_locale, is_class, ...} =>
+    {target = target, is_locale = is_locale, is_class = is_class}) (Data.get lthy)
+  else NONE;
 
-fun is_theory lthy =
-  Option.map #target (peek lthy) = SOME "" andalso Local_Theory.level lthy = 1;
+fun is_theory lthy = Option.map #target (peek lthy) = SOME "";
 
 
 (* define *)