# HG changeset patch
# User haftmann
# Date 1402121763 -7200
# Node ID 79d43c510b84c3d7b04d7d9ad0aa4f81553e2ee1
# Parent  2d13bf9ea77b9dd9b9106664270b26bc8ae31385
less baroque interface

diff -r 2d13bf9ea77b -r 79d43c510b84 src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Fri Jun 06 19:19:46 2014 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Sat Jun 07 08:16:03 2014 +0200
@@ -346,10 +346,9 @@
   let
     val thy = Proof_Context.theory_of lthy;
     val proto_sup = prep_class thy raw_sup;
-    val proto_sub =
-      (case Named_Target.peek lthy of
-         SOME {target, is_class = true, ...} => target
-      | _ => error "Not in a class target");
+    val proto_sub = case Named_Target.class_of lthy of
+        SOME class => class
+      | NONE => error "Not in a class target";
     val (sub, sup) = Axclass.cert_classrel thy (proto_sub, proto_sup);
 
     val expr = ([(sup, (("", false), Expression.Positional []))], []);
diff -r 2d13bf9ea77b -r 79d43c510b84 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Fri Jun 06 19:19:46 2014 +0200
+++ b/src/Pure/Isar/named_target.ML	Sat Jun 07 08:16:03 2014 +0200
@@ -7,8 +7,9 @@
 
 signature NAMED_TARGET =
 sig
-  val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option
   val is_theory: local_theory -> bool
+  val 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
   val reinit: local_theory -> local_theory -> local_theory
@@ -40,12 +41,21 @@
 
 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)
+  then Option.map (fn Target ta => ta) (Data.get lthy)
   else NONE;
 
 fun is_theory lthy = Option.map #target (peek lthy) = SOME "";
 
+fun locale_of lthy =
+  case peek lthy of
+    SOME {target = locale, is_locale = true, ...} => SOME locale
+  | _ => NONE;
+
+fun class_of lthy =
+  case peek lthy of
+    SOME {target = class, is_class = true, ...} => SOME class
+  | _ => NONE;
+
 
 (* define *)
 
diff -r 2d13bf9ea77b -r 79d43c510b84 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Fri Jun 06 19:19:46 2014 +0200
+++ b/src/Tools/quickcheck.ML	Sat Jun 07 08:16:03 2014 +0200
@@ -362,11 +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 =
-      (case (Option.map #target o Named_Target.peek) lthy of
-        NONE => NONE
-      | SOME "" => NONE
-      | SOME locale => SOME locale);
+    val some_locale = Named_Target.locale_of lthy;
     val assms =
       if Config.get lthy no_assms then []
       else