# HG changeset patch
# User blanchet
# Date 1284540322 -7200
# Node ID fcbb3bb3ebe2b2ac9e1946cd1b666553678372ad
# Parent  0049301f7333027d235abcef53eb9ba6fcf1384e# Parent  ddfafa97da2f36b008a189bc80c90ecf15c68b44
merge

diff -r 0049301f7333 -r fcbb3bb3ebe2 src/HOL/Library/AssocList.thy
--- a/src/HOL/Library/AssocList.thy	Wed Sep 15 10:43:57 2010 +0200
+++ b/src/HOL/Library/AssocList.thy	Wed Sep 15 10:45:22 2010 +0200
@@ -701,37 +701,13 @@
   "Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
   by (rule mapping_eqI) (simp add: map_of_map_restrict fun_eq_iff)
 
-lemma map_of_eqI: (*FIXME move to Map.thy*)
-  assumes set_eq: "set (map fst xs) = set (map fst ys)"
-  assumes map_eq: "\<forall>k\<in>set (map fst xs). map_of xs k = map_of ys k"
-  shows "map_of xs = map_of ys"
-proof (rule ext)
-  fix k show "map_of xs k = map_of ys k"
-  proof (cases "map_of xs k")
-    case None then have "k \<notin> set (map fst xs)" by (simp add: map_of_eq_None_iff)
-    with set_eq have "k \<notin> set (map fst ys)" by simp
-    then have "map_of ys k = None" by (simp add: map_of_eq_None_iff)
-    with None show ?thesis by simp
-  next
-    case (Some v) then have "k \<in> set (map fst xs)" by (auto simp add: dom_map_of_conv_image_fst [symmetric])
-    with map_eq show ?thesis by auto
-  qed
-qed
-
-lemma map_of_eq_dom: (*FIXME move to Map.thy*)
-  assumes "map_of xs = map_of ys"
-  shows "fst ` set xs = fst ` set ys"
-proof -
-  from assms have "dom (map_of xs) = dom (map_of ys)" by simp
-  then show ?thesis by (simp add: dom_map_of_conv_image_fst)
-qed
-
 lemma equal_Mapping [code]:
   "HOL.equal (Mapping xs) (Mapping ys) \<longleftrightarrow>
     (let ks = map fst xs; ls = map fst ys
     in (\<forall>l\<in>set ls. l \<in> set ks) \<and> (\<forall>k\<in>set ks. k \<in> set ls \<and> map_of xs k = map_of ys k))"
 proof -
-  have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs" by (auto simp add: image_def intro!: bexI)
+  have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs"
+    by (auto simp add: image_def intro!: bexI)
   show ?thesis
     by (auto intro!: map_of_eqI simp add: Let_def equal Mapping_def)
       (auto dest!: map_of_eq_dom intro: aux)
diff -r 0049301f7333 -r fcbb3bb3ebe2 src/HOL/Library/Dlist.thy
--- a/src/HOL/Library/Dlist.thy	Wed Sep 15 10:43:57 2010 +0200
+++ b/src/HOL/Library/Dlist.thy	Wed Sep 15 10:45:22 2010 +0200
@@ -14,18 +14,20 @@
   show "[] \<in> ?dlist" by simp
 qed
 
-lemma dlist_ext:
-  assumes "list_of_dlist dxs = list_of_dlist dys"
-  shows "dxs = dys"
-  using assms by (simp add: list_of_dlist_inject)
+lemma dlist_eq_iff:
+  "dxs = dys \<longleftrightarrow> list_of_dlist dxs = list_of_dlist dys"
+  by (simp add: list_of_dlist_inject)
 
+lemma dlist_eqI:
+  "list_of_dlist dxs = list_of_dlist dys \<Longrightarrow> dxs = dys"
+  by (simp add: dlist_eq_iff)
 
 text {* Formal, totalized constructor for @{typ "'a dlist"}: *}
 
 definition Dlist :: "'a list \<Rightarrow> 'a dlist" where
   "Dlist xs = Abs_dlist (remdups xs)"
 
-lemma distinct_list_of_dlist [simp]:
+lemma distinct_list_of_dlist [simp, intro]:
   "distinct (list_of_dlist dxs)"
   using list_of_dlist [of dxs] by simp
 
diff -r 0049301f7333 -r fcbb3bb3ebe2 src/HOL/Library/Fset.thy
--- a/src/HOL/Library/Fset.thy	Wed Sep 15 10:43:57 2010 +0200
+++ b/src/HOL/Library/Fset.thy	Wed Sep 15 10:45:22 2010 +0200
@@ -20,15 +20,17 @@
   "Fset (member A) = A"
   by (fact member_inverse)
 
-declare member_inject [simp]
-
 lemma Fset_inject [simp]:
   "Fset A = Fset B \<longleftrightarrow> A = B"
   by (simp add: Fset_inject)
 
+lemma fset_eq_iff:
+  "A = B \<longleftrightarrow> member A = member B"
+  by (simp add: member_inject)
+
 lemma fset_eqI:
   "member A = member B \<Longrightarrow> A = B"
-  by simp
+  by (simp add: fset_eq_iff)
 
 declare mem_def [simp]
 
@@ -116,7 +118,7 @@
   [simp]: "A - B = Fset (member A - member B)"
 
 instance proof
-qed auto
+qed (auto intro: fset_eqI)
 
 end
 
@@ -234,7 +236,7 @@
   "HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a fset)"
 
 instance proof
-qed (simp add: equal_fset_def set_eq [symmetric])
+qed (simp add: equal_fset_def set_eq [symmetric] fset_eq_iff)
 
 end
 
diff -r 0049301f7333 -r fcbb3bb3ebe2 src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Wed Sep 15 10:43:57 2010 +0200
+++ b/src/HOL/Library/Mapping.thy	Wed Sep 15 10:45:22 2010 +0200
@@ -19,16 +19,17 @@
   "Mapping (lookup m) = m"
   by (fact lookup_inverse)
 
-declare lookup_inject [simp]
-
 lemma Mapping_inject [simp]:
   "Mapping f = Mapping g \<longleftrightarrow> f = g"
   by (simp add: Mapping_inject)
 
+lemma mapping_eq_iff:
+  "m = n \<longleftrightarrow> lookup m = lookup n"
+  by (simp add: lookup_inject)
+
 lemma mapping_eqI:
-  assumes "lookup m = lookup n"
-  shows "m = n"
-  using assms by simp
+  "lookup m = lookup n \<Longrightarrow> m = n"
+  by (simp add: mapping_eq_iff)
 
 definition empty :: "('a, 'b) mapping" where
   "empty = Mapping (\<lambda>_. None)"
@@ -287,7 +288,7 @@
   "HOL.equal m n \<longleftrightarrow> lookup m = lookup n"
 
 instance proof
-qed (simp add: equal_mapping_def)
+qed (simp add: equal_mapping_def mapping_eq_iff)
 
 end
 
diff -r 0049301f7333 -r fcbb3bb3ebe2 src/HOL/Library/RBT.thy
--- a/src/HOL/Library/RBT.thy	Wed Sep 15 10:43:57 2010 +0200
+++ b/src/HOL/Library/RBT.thy	Wed Sep 15 10:45:22 2010 +0200
@@ -16,15 +16,19 @@
   then show ?thesis ..
 qed
 
+lemma rbt_eq_iff:
+  "t1 = t2 \<longleftrightarrow> impl_of t1 = impl_of t2"
+  by (simp add: impl_of_inject)
+
+lemma rbt_eqI:
+  "impl_of t1 = impl_of t2 \<Longrightarrow> t1 = t2"
+  by (simp add: rbt_eq_iff)
+
 lemma is_rbt_impl_of [simp, intro]:
   "is_rbt (impl_of t)"
   using impl_of [of t] by simp
 
-lemma rbt_eq:
-  "t1 = t2 \<longleftrightarrow> impl_of t1 = impl_of t2"
-  by (simp add: impl_of_inject)
-
-lemma [code abstype]:
+lemma RBT_impl_of [simp, code abstype]:
   "RBT (impl_of t) = t"
   by (simp add: impl_of_inverse)
 
@@ -148,7 +152,7 @@
 
 lemma is_empty_empty [simp]:
   "is_empty t \<longleftrightarrow> t = empty"
-  by (simp add: rbt_eq is_empty_def impl_of_empty split: rbt.split)
+  by (simp add: rbt_eq_iff is_empty_def impl_of_empty split: rbt.split)
 
 lemma RBT_lookup_empty [simp]: (*FIXME*)
   "RBT_Impl.lookup t = Map.empty \<longleftrightarrow> t = RBT_Impl.Empty"
@@ -184,7 +188,7 @@
 
 lemma is_empty_Mapping [code]:
   "Mapping.is_empty (Mapping t) \<longleftrightarrow> is_empty t"
-  by (simp add: rbt_eq Mapping.is_empty_empty Mapping_def)
+  by (simp add: rbt_eq_iff Mapping.is_empty_empty Mapping_def)
 
 lemma insert_Mapping [code]:
   "Mapping.update k v (Mapping t) = Mapping (insert k v t)"
diff -r 0049301f7333 -r fcbb3bb3ebe2 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Wed Sep 15 10:43:57 2010 +0200
+++ b/src/HOL/Map.thy	Wed Sep 15 10:45:22 2010 +0200
@@ -568,6 +568,31 @@
   "set xs = dom m \<Longrightarrow> map_of (map (\<lambda>k. (k, the (m k))) xs) = m"
   by (rule ext) (auto simp add: map_of_map_restrict restrict_map_def)
 
+lemma map_of_eqI:
+  assumes set_eq: "set (map fst xs) = set (map fst ys)"
+  assumes map_eq: "\<forall>k\<in>set (map fst xs). map_of xs k = map_of ys k"
+  shows "map_of xs = map_of ys"
+proof (rule ext)
+  fix k show "map_of xs k = map_of ys k"
+  proof (cases "map_of xs k")
+    case None then have "k \<notin> set (map fst xs)" by (simp add: map_of_eq_None_iff)
+    with set_eq have "k \<notin> set (map fst ys)" by simp
+    then have "map_of ys k = None" by (simp add: map_of_eq_None_iff)
+    with None show ?thesis by simp
+  next
+    case (Some v) then have "k \<in> set (map fst xs)" by (auto simp add: dom_map_of_conv_image_fst [symmetric])
+    with map_eq show ?thesis by auto
+  qed
+qed
+
+lemma map_of_eq_dom:
+  assumes "map_of xs = map_of ys"
+  shows "fst ` set xs = fst ` set ys"
+proof -
+  from assms have "dom (map_of xs) = dom (map_of ys)" by simp
+  then show ?thesis by (simp add: dom_map_of_conv_image_fst)
+qed
+
 
 subsection {* @{term [source] ran} *}
 
diff -r 0049301f7333 -r fcbb3bb3ebe2 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Sep 15 10:43:57 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Wed Sep 15 10:45:22 2010 +0200
@@ -676,7 +676,7 @@
 
 val preprocess_options = Predicate_Compile_Aux.Options {
   expected_modes = NONE,
-  proposed_modes = NONE,
+  proposed_modes = [],
   proposed_names = [],
   show_steps = false,
   show_intermediate_results = false,
@@ -685,6 +685,7 @@
   show_mode_inference = false,
   show_compilation = false,
   show_caught_failures = false,
+  show_invalid_clauses = false,
   skip_proof = true,
   no_topmost_reordering = false,
   function_flattening = true,
diff -r 0049301f7333 -r fcbb3bb3ebe2 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Sep 15 10:43:57 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Sep 15 10:45:22 2010 +0200
@@ -139,16 +139,24 @@
         (Term_Graph.strong_conn gr) thy))
   end
 
-fun extract_options (((expected_modes, proposed_modes), (compilation, raw_options)), const) =
+datatype proposed_modes = Multiple_Preds of (string * (mode * string option) list) list
+  | Single_Pred of (mode * string option) list
+
+fun extract_options lthy (((expected_modes, proposed_modes), (compilation, raw_options)), const) =
   let
     fun chk s = member (op =) raw_options s
+    val proposed_modes = case proposed_modes of
+          Single_Pred proposed_modes => [(const, proposed_modes)]
+        | Multiple_Preds proposed_modes => map
+          (apfst (Code.read_const (ProofContext.theory_of lthy))) proposed_modes
   in
     Options {
       expected_modes = Option.map (pair const) expected_modes,
-      proposed_modes = Option.map (pair const o map fst) proposed_modes,
+      proposed_modes = 
+        map (apsnd (map fst)) proposed_modes,
       proposed_names =
-        the_default [] (Option.map (map_filter
-          (fn (m, NONE) => NONE | (m, SOME name) => SOME ((const, m), name))) proposed_modes),
+        maps (fn (predname, ms) => (map_filter
+          (fn (m, NONE) => NONE | (m, SOME name) => SOME ((predname, m), name))) ms) proposed_modes,
       show_steps = chk "show_steps",
       show_intermediate_results = chk "show_intermediate_results",
       show_proof_trace = chk "show_proof_trace",
@@ -156,6 +164,7 @@
       show_mode_inference = chk "show_mode_inference",
       show_compilation = chk "show_compilation",
       show_caught_failures = false,
+      show_invalid_clauses = chk "show_invalid_clauses",
       skip_proof = chk "skip_proof",
       function_flattening = not (chk "no_function_flattening"),
       specialise = chk "specialise",
@@ -174,7 +183,7 @@
      val const = Code.read_const thy raw_const
      val T = Sign.the_const_type thy const
      val t = Const (const, T)
-     val options = extract_options (((expected_modes, proposed_modes), raw_options), const)
+     val options = extract_options lthy (((expected_modes, proposed_modes), raw_options), const)
   in
     if is_inductify options then
       let
@@ -208,9 +217,13 @@
 val mode_and_opt_proposal = parse_mode_expr --
   Scan.optional (Args.$$$ "as" |-- Parse.xname >> SOME) NONE
 
+
 val opt_modes =
   Scan.optional (Parse.$$$ "(" |-- Args.$$$ "modes" |-- Parse.$$$ ":" |--
-    Parse.enum "," mode_and_opt_proposal --| Parse.$$$ ")" >> SOME) NONE
+    (((Parse.enum1 "and" (Parse.xname --| Parse.$$$ ":" --
+        (Parse.enum "," mode_and_opt_proposal))) >> Multiple_Preds)
+      || ((Parse.enum "," mode_and_opt_proposal) >> Single_Pred))
+    --| Parse.$$$ ")") (Multiple_Preds [])
 
 val opt_expected_modes =
   Scan.optional (Parse.$$$ "(" |-- Args.$$$ "expected_modes" |-- Parse.$$$ ":" |--
diff -r 0049301f7333 -r fcbb3bb3ebe2 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Sep 15 10:43:57 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Sep 15 10:45:22 2010 +0200
@@ -99,7 +99,7 @@
   (* Different options for compiler *)
   datatype options = Options of {  
     expected_modes : (string * mode list) option,
-    proposed_modes : (string * mode list) option,
+    proposed_modes : (string * mode list) list,
     proposed_names : ((string * mode) * string) list,
     show_steps : bool,
     show_proof_trace : bool,
@@ -108,6 +108,7 @@
     show_modes : bool,
     show_compilation : bool,
     show_caught_failures : bool,
+    show_invalid_clauses : bool,
     skip_proof : bool,
     no_topmost_reordering : bool,
     function_flattening : bool,
@@ -119,7 +120,7 @@
     compilation : compilation
   };
   val expected_modes : options -> (string * mode list) option
-  val proposed_modes : options -> (string * mode list) option
+  val proposed_modes : options -> string -> mode list option
   val proposed_names : options -> string -> mode -> string option
   val show_steps : options -> bool
   val show_proof_trace : options -> bool
@@ -128,6 +129,7 @@
   val show_modes : options -> bool
   val show_compilation : options -> bool
   val show_caught_failures : options -> bool
+  val show_invalid_clauses : options -> bool
   val skip_proof : options -> bool
   val no_topmost_reordering : options -> bool
   val function_flattening : options -> bool
@@ -703,7 +705,7 @@
 
 datatype options = Options of {  
   expected_modes : (string * mode list) option,
-  proposed_modes : (string * mode list) option,
+  proposed_modes : (string * mode list) list,
   proposed_names : ((string * mode) * string) list,
   show_steps : bool,
   show_proof_trace : bool,
@@ -712,6 +714,7 @@
   show_modes : bool,
   show_compilation : bool,
   show_caught_failures : bool,
+  show_invalid_clauses : bool,
   skip_proof : bool,
   no_topmost_reordering : bool,
   function_flattening : bool,
@@ -724,7 +727,7 @@
 };
 
 fun expected_modes (Options opt) = #expected_modes opt
-fun proposed_modes (Options opt) = #proposed_modes opt
+fun proposed_modes (Options opt) = AList.lookup (op =) (#proposed_modes opt)
 fun proposed_names (Options opt) name mode = AList.lookup (eq_pair (op =) eq_mode)
   (#proposed_names opt) (name, mode)
 
@@ -735,7 +738,7 @@
 fun show_mode_inference (Options opt) = #show_mode_inference opt
 fun show_compilation (Options opt) = #show_compilation opt
 fun show_caught_failures (Options opt) = #show_caught_failures opt
-
+fun show_invalid_clauses (Options opt) = #show_invalid_clauses opt
 fun skip_proof (Options opt) = #skip_proof opt
 
 fun function_flattening (Options opt) = #function_flattening opt
@@ -752,7 +755,7 @@
 
 val default_options = Options {
   expected_modes = NONE,
-  proposed_modes = NONE,
+  proposed_modes = [],
   proposed_names = [],
   show_steps = false,
   show_intermediate_results = false,
@@ -761,6 +764,7 @@
   show_mode_inference = false,
   show_compilation = false,
   show_caught_failures = false,
+  show_invalid_clauses = false,
   skip_proof = true,
   no_topmost_reordering = false,
   function_flattening = false,
@@ -773,8 +777,8 @@
 }
 
 val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes",
-  "show_mode_inference", "show_compilation", "skip_proof", "inductify", "no_function_flattening",
-  "detect_switches", "specialise", "no_topmost_reordering"]
+  "show_mode_inference", "show_compilation", "show_invalid_clauses", "skip_proof", "inductify",
+  "no_function_flattening", "detect_switches", "specialise", "no_topmost_reordering"]
 
 fun print_step options s =
   if show_steps options then tracing s else ()
diff -r 0049301f7333 -r fcbb3bb3ebe2 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Sep 15 10:43:57 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Sep 15 10:45:22 2010 +0200
@@ -400,8 +400,8 @@
   | NONE => ()
 
 fun check_proposed_modes preds options modes errors =
-  case proposed_modes options of
-    SOME (s, ms) => (case AList.lookup (op =) modes s of
+  map (fn (s, _) => case proposed_modes options s of
+    SOME ms => (case AList.lookup (op =) modes s of
       SOME inferred_ms =>
         let
           val preds_without_modes = map fst (filter (null o snd) modes)
@@ -411,15 +411,16 @@
             error ("expected modes were not inferred:\n"
             ^ "  inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode modes')  ^ "\n"
             ^ "  expected modes for " ^ s ^ ": " ^ commas (map string_of_mode ms) ^ "\n"
-            ^ "For the following clauses, the following modes could not be inferred: " ^ "\n"
-            ^ cat_lines errors ^
+            ^ (if show_invalid_clauses options then
+            ("For the following clauses, the following modes could not be inferred: " ^ "\n"
+            ^ cat_lines errors) else "") ^
             (if not (null preds_without_modes) then
               "\n" ^ "No mode inferred for the predicates " ^ commas preds_without_modes
             else ""))
           else ()
         end
       | NONE => ())
-  | NONE => ()
+  | NONE => ()) preds
 
 (* importing introduction rules *)
 
@@ -1503,7 +1504,6 @@
 fun infer_modes mode_analysis_options options (lookup_mode, lookup_neg_mode, needs_random) ctxt
   preds all_modes param_vs clauses =
   let
-    val collect_errors = false
     fun appair f (x1, x2) (y1, y2) = (f x1 y1, f x2 y2)
     fun add_needs_random s (false, m) = ((false, m), false)
       | add_needs_random s (true, m) = ((true, m), needs_random s m)
@@ -1549,7 +1549,7 @@
         (modes @ extra_modes)) modes
     val ((modes : (string * ((bool * mode) * bool) list) list), errors) =
       Output.cond_timeit false "Fixpount computation of mode analysis" (fn () =>
-      if collect_errors then
+      if show_invalid_clauses options then
         fixp_with_state (fn (modes, errors) =>
           let
             val (modes', new_errors) = split_list (iteration modes)
@@ -2700,8 +2700,8 @@
         all_modes_of_typ T
     val all_modes = 
       map (fn (s, T) =>
-        (s, case (proposed_modes options) of
-            SOME (s', ms) => if s = s' then ms else generate_modes s T
+        (s, case proposed_modes options s of
+            SOME ms => ms
           | NONE => generate_modes s T)) preds
     val params =
       case intrs of
@@ -2719,7 +2719,7 @@
         let
           val (p, args) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl intr)) 
         in
-          ho_args_of (hd (the (AList.lookup (op =) all_modes (fst (dest_Const p))))) args
+          ho_args_of_typ (snd (dest_Const p)) args
         end
     val param_vs = map (fst o dest_Free) params
     fun add_clause intr clauses =
diff -r 0049301f7333 -r fcbb3bb3ebe2 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Sep 15 10:43:57 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Sep 15 10:45:22 2010 +0200
@@ -56,7 +56,7 @@
 
 val options = Options {
   expected_modes = NONE,
-  proposed_modes = NONE,
+  proposed_modes = [],
   proposed_names = [],
   show_steps = false,
   show_intermediate_results = false,
@@ -65,6 +65,7 @@
   show_mode_inference = false,
   show_compilation = false,
   show_caught_failures = false,
+  show_invalid_clauses = false, 
   skip_proof = false,
   compilation = Random,
   inductify = true,
@@ -78,7 +79,7 @@
 
 val debug_options = Options {
   expected_modes = NONE,
-  proposed_modes = NONE,
+  proposed_modes = [],
   proposed_names = [],
   show_steps = true,
   show_intermediate_results = true,
@@ -87,6 +88,7 @@
   show_mode_inference = true,
   show_compilation = false,
   show_caught_failures = true,
+  show_invalid_clauses = false,
   skip_proof = false,
   compilation = Random,
   inductify = true,
@@ -102,13 +104,15 @@
 fun set_function_flattening b
   (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
     show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
-    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
+    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
+    show_invalid_clauses = s_ic, skip_proof = s_p,
     compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, 
     fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
     no_topmost_reordering = re}) =
   (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
     show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
-    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
+    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
+    show_invalid_clauses = s_ic, skip_proof = s_p,
     compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = b,
     fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
     no_topmost_reordering = re})
@@ -116,13 +120,15 @@
 fun set_fail_safe_function_flattening b
   (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
     show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
-    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
+    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
+    show_invalid_clauses = s_ic, skip_proof = s_p,
     compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, 
     fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
     no_topmost_reordering = re}) =
   (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
     show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
-    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
+    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
+    show_invalid_clauses = s_ic, skip_proof = s_p,
     compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
     fail_safe_function_flattening = b, no_higher_order_predicate = no_ho,
     no_topmost_reordering = re})
@@ -130,13 +136,15 @@
 fun set_no_higher_order_predicate ss
   (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
     show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
-    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
+    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
+    show_invalid_clauses = s_ic, skip_proof = s_p,
     compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f, 
     fail_safe_function_flattening = fs_ff, no_higher_order_predicate = no_ho,
     no_topmost_reordering = re}) =
   (Options { expected_modes = e_m, proposed_modes = p_m, proposed_names = p_n, show_steps = s_s,
     show_intermediate_results = s_ir, show_proof_trace = s_pt, show_modes = s_m,
-    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf, skip_proof = s_p,
+    show_mode_inference = s_mi, show_compilation = s_c, show_caught_failures = s_cf,
+    show_invalid_clauses = s_ic, skip_proof = s_p,
     compilation = c, inductify = i, specialise = sp, detect_switches = ds, function_flattening = f_f,
     fail_safe_function_flattening = fs_ff, no_higher_order_predicate = ss, no_topmost_reordering = re})
 
diff -r 0049301f7333 -r fcbb3bb3ebe2 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Sep 15 10:43:57 2010 +0200
+++ b/src/Pure/Isar/class.ML	Wed Sep 15 10:45:22 2010 +0200
@@ -293,7 +293,7 @@
   |> Variable.declare_term
       (Logic.mk_type (TFree (Name.aT, base_sort)))
   |> synchronize_class_syntax sort base_sort
-  |> Overloading.add_improvable_syntax;
+  |> Overloading.activate_improvable_syntax;
 
 fun init class thy =
   thy
@@ -548,7 +548,7 @@
     |> fold (Variable.declare_names o Free o snd) params
     |> (Overloading.map_improvable_syntax o apfst)
          (K ((primary_constraints, []), (((improve, K NONE), false), [])))
-    |> Overloading.add_improvable_syntax
+    |> Overloading.activate_improvable_syntax
     |> Context.proof_map (Syntax.add_term_check 0 "resorting" resort_check)
     |> synchronize_inst_syntax
     |> Local_Theory.init NONE ""
diff -r 0049301f7333 -r fcbb3bb3ebe2 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Wed Sep 15 10:43:57 2010 +0200
+++ b/src/Pure/Isar/overloading.ML	Wed Sep 15 10:45:22 2010 +0200
@@ -7,7 +7,7 @@
 signature OVERLOADING =
 sig
   type improvable_syntax
-  val add_improvable_syntax: Proof.context -> Proof.context
+  val activate_improvable_syntax: Proof.context -> Proof.context
   val map_improvable_syntax: (improvable_syntax -> improvable_syntax)
     -> Proof.context -> Proof.context
   val set_primary_constraints: Proof.context -> Proof.context
@@ -104,7 +104,7 @@
     val { primary_constraints, ... } = ImprovableSyntax.get ctxt;
   in fold (ProofContext.add_const_constraint o apsnd SOME) primary_constraints ctxt end;
 
-val add_improvable_syntax =
+val activate_improvable_syntax =
   Context.proof_map
     (Syntax.add_term_check 0 "improvement" improve_term_check
     #> Syntax.add_term_uncheck 0 "improvement" improve_term_uncheck)
@@ -183,7 +183,7 @@
     |> ProofContext.init_global
     |> Data.put overloading
     |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
-    |> add_improvable_syntax
+    |> activate_improvable_syntax
     |> synchronize_syntax
     |> Local_Theory.init NONE ""
        {define = Generic_Target.define foundation,