# 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