# HG changeset patch
# User haftmann
# Date 1401989978 -7200
# Node ID dce365931721669fc81360bf01bb82eb31460d2b
# Parent  88739947cc738f1170407cb9bf1b79267575a87f
sharpened criterion: bare named target is only at the bottom level

diff -r 88739947cc73 -r dce365931721 src/Pure/Isar/named_target.ML
--- 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 *)