# HG changeset patch
# User haftmann
# Date 1402263052 -7200
# Node ID ec0e10f1127676669a52dbaac7daf6f636af4f57
# Parent  d110b0d1bc12ed762d3b2b753a459f84c4123aad
recovered level-free fishing for locale, accidentally lost in dce365931721

diff -r d110b0d1bc12 -r ec0e10f11276 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Sun Jun 08 23:30:52 2014 +0200
+++ b/src/Pure/Isar/named_target.ML	Sun Jun 08 23:30:52 2014 +0200
@@ -9,6 +9,7 @@
 sig
   val is_theory: local_theory -> bool
   val locale_of: local_theory -> string option
+  val bottom_locale_of: local_theory -> string option
   val class_of: local_theory -> string option
   val init: string -> theory -> local_theory
   val theory_init: theory -> local_theory
@@ -38,23 +39,30 @@
   fun init _ = NONE;
 );
 
-fun peek lthy =
+val get_bottom_data = Option.map (fn Target ta => ta) o Data.get;
+
+fun get_data lthy =
   if Local_Theory.level lthy = 1
-  then Option.map (fn Target ta => ta) (Data.get lthy)
+  then get_bottom_data lthy
   else NONE;
 
 fun is_theory lthy =
-  case peek lthy of
+  case get_data lthy of
     SOME {target = "", ...} => true
   | _ => false;
 
 fun locale_of lthy =
-  case peek lthy of
+  case get_data lthy of
+    SOME {target = locale, is_locale = true, ...} => SOME locale
+  | _ => NONE;
+
+fun bottom_locale_of lthy =
+  case get_bottom_data lthy of
     SOME {target = locale, is_locale = true, ...} => SOME locale
   | _ => NONE;
 
 fun class_of lthy =
-  case peek lthy of
+  case get_data lthy of
     SOME {target = class, is_class = true, ...} => SOME class
   | _ => NONE;
 
diff -r d110b0d1bc12 -r ec0e10f11276 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Sun Jun 08 23:30:52 2014 +0200
+++ b/src/Tools/quickcheck.ML	Sun Jun 08 23:30:52 2014 +0200
@@ -362,7 +362,7 @@
       | strip t = t;
     val {goal = st, ...} = Proof.raw_goal state;
     val (gi, frees) = Logic.goal_params (prop_of st) i;
-    val some_locale = Named_Target.locale_of lthy;
+    val some_locale = Named_Target.bottom_locale_of lthy;
     val assms =
       if Config.get lthy no_assms then []
       else