# HG changeset patch
# User haftmann
# Date 1402121763 -7200
# Node ID 188da8aaae24a089274852f0a1a1d46e7934872e
# Parent  56f3351cc492d3580ef000b38bc68df4b74a7b20
tuned

diff -r 56f3351cc492 -r 188da8aaae24 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Sat Jun 07 08:16:03 2014 +0200
+++ b/src/Pure/Isar/named_target.ML	Sat Jun 07 08:16:03 2014 +0200
@@ -43,7 +43,10 @@
   then Option.map (fn Target ta => ta) (Data.get lthy)
   else NONE;
 
-fun is_theory lthy = Option.map #target (peek lthy) = SOME "";
+fun is_theory lthy =
+  case peek lthy of
+    SOME {target = "", ...} => true
+  | _ => false;
 
 fun locale_of lthy =
   case peek lthy of