less baroque interface
authorhaftmann
Sat Jun 07 08:16:03 2014 +0200 (2014-06-07)
changeset 5718279d43c510b84
parent 57181 2d13bf9ea77b
child 57183 766e7f50c22f
less baroque interface
src/Pure/Isar/class_declaration.ML
src/Pure/Isar/named_target.ML
src/Tools/quickcheck.ML
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Fri Jun 06 19:19:46 2014 +0200
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Sat Jun 07 08:16:03 2014 +0200
     1.3 @@ -346,10 +346,9 @@
     1.4    let
     1.5      val thy = Proof_Context.theory_of lthy;
     1.6      val proto_sup = prep_class thy raw_sup;
     1.7 -    val proto_sub =
     1.8 -      (case Named_Target.peek lthy of
     1.9 -         SOME {target, is_class = true, ...} => target
    1.10 -      | _ => error "Not in a class target");
    1.11 +    val proto_sub = case Named_Target.class_of lthy of
    1.12 +        SOME class => class
    1.13 +      | NONE => error "Not in a class target";
    1.14      val (sub, sup) = Axclass.cert_classrel thy (proto_sub, proto_sup);
    1.15  
    1.16      val expr = ([(sup, (("", false), Expression.Positional []))], []);
     2.1 --- a/src/Pure/Isar/named_target.ML	Fri Jun 06 19:19:46 2014 +0200
     2.2 +++ b/src/Pure/Isar/named_target.ML	Sat Jun 07 08:16:03 2014 +0200
     2.3 @@ -7,8 +7,9 @@
     2.4  
     2.5  signature NAMED_TARGET =
     2.6  sig
     2.7 -  val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option
     2.8    val is_theory: local_theory -> bool
     2.9 +  val locale_of: local_theory -> string option
    2.10 +  val class_of: local_theory -> string option
    2.11    val init: string -> theory -> local_theory
    2.12    val theory_init: theory -> local_theory
    2.13    val reinit: local_theory -> local_theory -> local_theory
    2.14 @@ -40,12 +41,21 @@
    2.15  
    2.16  fun peek lthy =
    2.17    if Local_Theory.level lthy = 1
    2.18 -  then Option.map (fn Target {target, is_locale, is_class, ...} =>
    2.19 -    {target = target, is_locale = is_locale, is_class = is_class}) (Data.get lthy)
    2.20 +  then Option.map (fn Target ta => ta) (Data.get lthy)
    2.21    else NONE;
    2.22  
    2.23  fun is_theory lthy = Option.map #target (peek lthy) = SOME "";
    2.24  
    2.25 +fun locale_of lthy =
    2.26 +  case peek lthy of
    2.27 +    SOME {target = locale, is_locale = true, ...} => SOME locale
    2.28 +  | _ => NONE;
    2.29 +
    2.30 +fun class_of lthy =
    2.31 +  case peek lthy of
    2.32 +    SOME {target = class, is_class = true, ...} => SOME class
    2.33 +  | _ => NONE;
    2.34 +
    2.35  
    2.36  (* define *)
    2.37  
     3.1 --- a/src/Tools/quickcheck.ML	Fri Jun 06 19:19:46 2014 +0200
     3.2 +++ b/src/Tools/quickcheck.ML	Sat Jun 07 08:16:03 2014 +0200
     3.3 @@ -362,11 +362,7 @@
     3.4        | strip t = t;
     3.5      val {goal = st, ...} = Proof.raw_goal state;
     3.6      val (gi, frees) = Logic.goal_params (prop_of st) i;
     3.7 -    val some_locale =
     3.8 -      (case (Option.map #target o Named_Target.peek) lthy of
     3.9 -        NONE => NONE
    3.10 -      | SOME "" => NONE
    3.11 -      | SOME locale => SOME locale);
    3.12 +    val some_locale = Named_Target.locale_of lthy;
    3.13      val assms =
    3.14        if Config.get lthy no_assms then []
    3.15        else