--- 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 []))], []);
--- 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 *)
--- 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