# 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);