# HG changeset patch # User haftmann # Date 1281613332 -7200 # Node ID cb72d89bb444d2e49cac6e078a555bccd56fe6c5 # Parent d7d915bae307046ff2ce1357bc6acc17e26e0a07 named target is optional diff -r d7d915bae307 -r cb72d89bb444 src/Pure/Isar/class_declaration.ML --- a/src/Pure/Isar/class_declaration.ML Thu Aug 12 13:28:18 2010 +0200 +++ b/src/Pure/Isar/class_declaration.ML Thu Aug 12 13:42:12 2010 +0200 @@ -311,8 +311,8 @@ val thy = ProofContext.theory_of lthy; val proto_sup = prep_class thy raw_sup; val proto_sub = case Named_Target.peek lthy - of {is_class = false, ...} => error "Not in a class context" - | {target, ...} => target; + of SOME {target, is_class = true, ...} => target + | _ => 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 d7d915bae307 -r cb72d89bb444 src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Thu Aug 12 13:28:18 2010 +0200 +++ b/src/Tools/quickcheck.ML Thu Aug 12 13:42:12 2010 +0200 @@ -219,9 +219,10 @@ | strip t = t; val {goal = st, ...} = Proof.raw_goal state; val (gi, frees) = Logic.goal_params (prop_of st) i; - val some_locale = case (#target o Named_Target.peek) lthy - of "" => NONE - | locale => SOME locale; + val some_locale = case (Option.map #target o Named_Target.peek) lthy + of NONE => NONE + | SOME "" => NONE + | SOME locale => SOME locale; val assms = if no_assms then [] else case some_locale of NONE => Assumption.all_assms_of lthy | SOME locale => Assumption.local_assms_of lthy (Locale.init locale thy);