named target is optional
authorhaftmann
Thu Aug 12 13:42:12 2010 +0200 (2010-08-12 ago)
changeset 38390cb72d89bb444
parent 38389 d7d915bae307
child 38391 ba1cc1815ce1
named target is optional
src/Pure/Isar/class_declaration.ML
src/Tools/quickcheck.ML
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Thu Aug 12 13:28:18 2010 +0200
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Thu Aug 12 13:42:12 2010 +0200
     1.3 @@ -311,8 +311,8 @@
     1.4      val thy = ProofContext.theory_of lthy;
     1.5      val proto_sup = prep_class thy raw_sup;
     1.6      val proto_sub = case Named_Target.peek lthy
     1.7 -     of {is_class = false, ...} => error "Not in a class context"
     1.8 -      | {target, ...} => target;
     1.9 +     of SOME {target, is_class = true, ...} => target
    1.10 +      | _ => error "Not in a class target";
    1.11      val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup);
    1.12  
    1.13      val expr = ([(sup, (("", false), Expression.Positional []))], []);
     2.1 --- a/src/Tools/quickcheck.ML	Thu Aug 12 13:28:18 2010 +0200
     2.2 +++ b/src/Tools/quickcheck.ML	Thu Aug 12 13:42:12 2010 +0200
     2.3 @@ -219,9 +219,10 @@
     2.4        | strip t = t;
     2.5      val {goal = st, ...} = Proof.raw_goal state;
     2.6      val (gi, frees) = Logic.goal_params (prop_of st) i;
     2.7 -    val some_locale = case (#target o Named_Target.peek) lthy
     2.8 -     of "" => NONE
     2.9 -      | locale => SOME locale;
    2.10 +    val some_locale = case (Option.map #target o Named_Target.peek) lthy
    2.11 +     of NONE => NONE
    2.12 +      | SOME "" => NONE
    2.13 +      | SOME locale => SOME locale;
    2.14      val assms = if no_assms then [] else case some_locale
    2.15       of NONE => Assumption.all_assms_of lthy
    2.16        | SOME locale => Assumption.local_assms_of lthy (Locale.init locale thy);