# HG changeset patch
# User blanchet
# Date 1272628847 -7200
# Node ID ed99188882b13c6bd2087a659140d5cc698d3ebd
# Parent  2a9d0ec8c10d1d087f3c2488434bef4e6a3d3d23# Parent  16ec4fe058cb70c8c835a3ef6e60b627353748a5
merged

diff -r 2a9d0ec8c10d -r ed99188882b1 src/HOL/Metis_Examples/Abstraction.thy
--- a/src/HOL/Metis_Examples/Abstraction.thy	Fri Apr 30 13:47:39 2010 +0200
+++ b/src/HOL/Metis_Examples/Abstraction.thy	Fri Apr 30 14:00:47 2010 +0200
@@ -23,13 +23,11 @@
 
 declare [[ atp_problem_prefix = "Abstraction__Collect_triv" ]]
 lemma (*Collect_triv:*) "a \<in> {x. P x} ==> P a"
-proof (neg_clausify)
-assume 0: "(a\<Colon>'a\<Colon>type) \<in> Collect (P\<Colon>'a\<Colon>type \<Rightarrow> bool)"
-assume 1: "\<not> (P\<Colon>'a\<Colon>type \<Rightarrow> bool) (a\<Colon>'a\<Colon>type)"
-have 2: "(P\<Colon>'a\<Colon>type \<Rightarrow> bool) (a\<Colon>'a\<Colon>type)"
-  by (metis CollectD 0)
-show "False"
-  by (metis 2 1)
+proof -
+  assume "a \<in> {x. P x}"
+  hence "a \<in> P" by (metis Collect_def)
+  hence "P a" by (metis mem_def)
+  thus "P a" by metis
 qed
 
 lemma Collect_triv: "a \<in> {x. P x} ==> P a"
@@ -38,76 +36,52 @@
 
 declare [[ atp_problem_prefix = "Abstraction__Collect_mp" ]]
 lemma "a \<in> {x. P x --> Q x} ==> a \<in> {x. P x} ==> a \<in> {x. Q x}"
-  by (metis CollectI Collect_imp_eq ComplD UnE mem_Collect_eq);
-  --{*34 secs*}
+  by (metis Collect_imp_eq ComplD UnE)
 
 declare [[ atp_problem_prefix = "Abstraction__Sigma_triv" ]]
 lemma "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a"
-proof (neg_clausify)
-assume 0: "(a\<Colon>'a\<Colon>type, b\<Colon>'b\<Colon>type) \<in> Sigma (A\<Colon>'a\<Colon>type set) (B\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>type set)"
-assume 1: "(a\<Colon>'a\<Colon>type) \<notin> (A\<Colon>'a\<Colon>type set) \<or> (b\<Colon>'b\<Colon>type) \<notin> (B\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>type set) a"
-have 2: "(a\<Colon>'a\<Colon>type) \<in> (A\<Colon>'a\<Colon>type set)"
-  by (metis SigmaD1 0)
-have 3: "(b\<Colon>'b\<Colon>type) \<in> (B\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>type set) (a\<Colon>'a\<Colon>type)"
-  by (metis SigmaD2 0)
-have 4: "(b\<Colon>'b\<Colon>type) \<notin> (B\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>type set) (a\<Colon>'a\<Colon>type)"
-  by (metis 1 2)
-show "False"
-  by (metis 3 4)
+proof -
+  assume A1: "(a, b) \<in> Sigma A B"
+  hence F1: "b \<in> B a" by (metis mem_Sigma_iff)
+  have F2: "a \<in> A" by (metis A1 mem_Sigma_iff)
+  have "b \<in> B a" by (metis F1)
+  thus "a \<in> A \<and> b \<in> B a" by (metis F2)
 qed
 
 lemma Sigma_triv: "(a,b) \<in> Sigma A B ==> a \<in> A & b \<in> B a"
 by (metis SigmaD1 SigmaD2)
 
 declare [[ atp_problem_prefix = "Abstraction__Sigma_Collect" ]]
-lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
-(*???metis says this is satisfiable!
+lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
+(* Metis says this is satisfiable!
 by (metis CollectD SigmaD1 SigmaD2)
 *)
 by (meson CollectD SigmaD1 SigmaD2)
 
 
-(*single-step*)
-lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
-by (metis SigmaD1 SigmaD2 insert_def singleton_conv2 Un_empty_right vimage_Collect_eq vimage_def vimage_singleton_eq)
-
+lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
+by (metis mem_Sigma_iff singleton_conv2 vimage_Collect_eq vimage_singleton_eq)
 
-lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
-proof (neg_clausify)
-assume 0: "(a\<Colon>'a\<Colon>type, b\<Colon>'b\<Colon>type)
-\<in> Sigma (A\<Colon>'a\<Colon>type set)
-   (COMBB Collect (COMBC (COMBB COMBB op =) (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type)))"
-assume 1: "(a\<Colon>'a\<Colon>type) \<notin> (A\<Colon>'a\<Colon>type set) \<or> a \<noteq> (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type) (b\<Colon>'b\<Colon>type)"
-have 2: "(a\<Colon>'a\<Colon>type) \<in> (A\<Colon>'a\<Colon>type set)"
-  by (metis 0 SigmaD1)
-have 3: "(b\<Colon>'b\<Colon>type)
-\<in> COMBB Collect (COMBC (COMBB COMBB op =) (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type)) (a\<Colon>'a\<Colon>type)"
-  by (metis 0 SigmaD2) 
-have 4: "(b\<Colon>'b\<Colon>type) \<in> Collect (COMBB (op = (a\<Colon>'a\<Colon>type)) (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type))"
-  by (metis 3)
-have 5: "(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type) (b\<Colon>'b\<Colon>type) \<noteq> (a\<Colon>'a\<Colon>type)"
-  by (metis 1 2)
-have 6: "(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>type) (b\<Colon>'b\<Colon>type) = (a\<Colon>'a\<Colon>type)"
-  by (metis 4 vimage_singleton_eq insert_def singleton_conv2 Un_empty_right vimage_Collect_eq vimage_def)
-show "False"
-  by (metis 5 6)
+lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
+proof -
+  assume A1: "(a, b) \<in> (SIGMA x:A. {y. x = f y})"
+  have F1: "\<forall>u. {u} = op = u" by (metis singleton_conv2 Collect_def)
+  have F2: "\<forall>y w v. v \<in> w -` op = y \<longrightarrow> w v = y"
+    by (metis F1 vimage_singleton_eq)
+  have F3: "\<forall>x w. (\<lambda>R. w (x R)) = x -` w"
+    by (metis vimage_Collect_eq Collect_def)
+  show "a \<in> A \<and> a = f b" by (metis A1 F2 F3 mem_Sigma_iff Collect_def)
 qed
 
-(*Alternative structured proof, untyped*)
-lemma "(a,b) \<in> (SIGMA x: A. {y. x = f y}) ==> a \<in> A & a = f b"
-proof (neg_clausify)
-assume 0: "(a, b) \<in> Sigma A (COMBB Collect (COMBC (COMBB COMBB op =) f))"
-have 1: "b \<in> Collect (COMBB (op = a) f)"
-  by (metis 0 SigmaD2)
-have 2: "f b = a"
-  by (metis 1 vimage_Collect_eq singleton_conv2 insert_def Un_empty_right vimage_singleton_eq vimage_def)
-assume 3: "a \<notin> A \<or> a \<noteq> f b"
-have 4: "a \<in> A"
-  by (metis 0 SigmaD1)
-have 5: "f b \<noteq> a"
-  by (metis 4 3)
-show "False"
-  by (metis 5 2)
+(* Alternative structured proof *)
+lemma "(a, b) \<in> (SIGMA x:A. {y. x = f y}) \<Longrightarrow> a \<in> A \<and> a = f b"
+proof -
+  assume A1: "(a, b) \<in> (SIGMA x:A. {y. x = f y})"
+  hence F1: "a \<in> A" by (metis mem_Sigma_iff)
+  have "b \<in> {R. a = f R}" by (metis A1 mem_Sigma_iff)
+  hence F2: "b \<in> (\<lambda>R. a = f R)" by (metis Collect_def)
+  hence "a = f b" by (unfold mem_def)
+  thus "a \<in> A \<and> a = f b" by (metis F1)
 qed
 
 
@@ -116,56 +90,40 @@
 by (metis Collect_mem_eq SigmaD2)
 
 lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"
-proof (neg_clausify)
-assume 0: "(cl, f) \<in> CLF"
-assume 1: "CLF = Sigma CL (COMBB Collect (COMBB (COMBC op \<in>) pset))"
-assume 2: "f \<notin> pset cl"
-have 3: "\<And>X1 X2. X2 \<in> COMBB Collect (COMBB (COMBC op \<in>) pset) X1 \<or> (X1, X2) \<notin> CLF"
-  by (metis SigmaD2 1)
-have 4: "\<And>X1 X2. X2 \<in> pset X1 \<or> (X1, X2) \<notin> CLF"
-  by (metis 3 Collect_mem_eq)
-have 5: "(cl, f) \<notin> CLF"
-  by (metis 2 4)
-show "False"
-  by (metis 5 0)
+proof -
+  assume A1: "(cl, f) \<in> CLF"
+  assume A2: "CLF = (SIGMA cl:CL. {f. f \<in> pset cl})"
+  have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def)
+  have "\<forall>v u. (u, v) \<in> CLF \<longrightarrow> v \<in> {R. R \<in> pset u}" by (metis A2 mem_Sigma_iff)
+  hence "\<forall>v u. (u, v) \<in> CLF \<longrightarrow> v \<in> pset u" by (metis F1 Collect_def)
+  hence "f \<in> pset cl" by (metis A1)
+  thus "f \<in> pset cl" by metis
 qed
 
 declare [[ atp_problem_prefix = "Abstraction__Sigma_Collect_Pi" ]]
 lemma
     "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> 
     f \<in> pset cl \<rightarrow> pset cl"
-proof (neg_clausify)
-assume 0: "f \<notin> Pi (pset cl) (COMBK (pset cl))"
-assume 1: "(cl, f)
-\<in> Sigma CL
-   (COMBB Collect
-     (COMBB (COMBC op \<in>) (COMBS (COMBB Pi pset) (COMBB COMBK pset))))"
-show "False"
-(*  by (metis 0 Collect_mem_eq SigmaD2 1) ??doesn't terminate*)
-  by (insert 0 1, simp add: COMBB_def COMBS_def COMBC_def)
+proof -
+  assume A1: "(cl, f) \<in> (SIGMA cl:CL. {f. f \<in> pset cl \<rightarrow> pset cl})"
+  have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def)
+  have "f \<in> {R. R \<in> pset cl \<rightarrow> pset cl}" using A1 by simp
+  hence "f \<in> pset cl \<rightarrow> pset cl" by (metis F1 Collect_def)
+  thus "f \<in> pset cl \<rightarrow> pset cl" by metis
 qed
 
-
 declare [[ atp_problem_prefix = "Abstraction__Sigma_Collect_Int" ]]
 lemma
     "(cl,f) \<in> (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
    f \<in> pset cl \<inter> cl"
-proof (neg_clausify)
-assume 0: "(cl, f)
-\<in> Sigma CL
-   (COMBB Collect (COMBB (COMBC op \<in>) (COMBS (COMBB op \<inter> pset) COMBI)))"
-assume 1: "f \<notin> pset cl \<inter> cl"
-have 2: "f \<in> COMBB Collect (COMBB (COMBC op \<in>) (COMBS (COMBB op \<inter> pset) COMBI)) cl" 
-  by (insert 0, simp add: COMBB_def) 
-(*  by (metis SigmaD2 0)  ??doesn't terminate*)
-have 3: "f \<in> COMBS (COMBB op \<inter> pset) COMBI cl"
-  by (metis 2 Collect_mem_eq)
-have 4: "f \<notin> cl \<inter> pset cl"
-  by (metis 1 Int_commute)
-have 5: "f \<in> cl \<inter> pset cl"
-  by (metis 3 Int_commute)
-show "False"
-  by (metis 5 4)
+proof -
+  assume A1: "(cl, f) \<in> (SIGMA cl:CL. {f. f \<in> pset cl \<inter> cl})"
+  have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def)
+  have "f \<in> {R. R \<in> pset cl \<inter> cl}" using A1 by simp
+  hence "f \<in> Id_on cl `` pset cl" by (metis F1 Int_commute Image_Id_on Collect_def)
+  hence "f \<in> Id_on cl `` pset cl" by metis
+  hence "f \<in> cl \<inter> pset cl" by (metis Image_Id_on)
+  thus "f \<in> pset cl \<inter> cl" by (metis Int_commute)
 qed
 
 
@@ -181,19 +139,13 @@
    f \<in> pset cl \<inter> cl"
 by auto
 
-(*??no longer terminates, with combinators
-by (metis Collect_mem_eq Int_def SigmaD2 UnCI Un_absorb1)
-  --{*@{text Int_def} is redundant*}
-*)
 
 declare [[ atp_problem_prefix = "Abstraction__CLF_eq_Collect_Int" ]]
 lemma "(cl,f) \<in> CLF ==> 
    CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<inter> cl}) ==>
    f \<in> pset cl \<inter> cl"
 by auto
-(*??no longer terminates, with combinators
-by (metis Collect_mem_eq Int_commute SigmaD2)
-*)
+
 
 declare [[ atp_problem_prefix = "Abstraction__CLF_subset_Collect_Pi" ]]
 lemma 
@@ -201,9 +153,7 @@
     CLF \<subseteq> (SIGMA cl': CL. {f. f \<in> pset cl' \<rightarrow> pset cl'}) ==> 
     f \<in> pset cl \<rightarrow> pset cl"
 by fast
-(*??no longer terminates, with combinators
-by (metis Collect_mem_eq SigmaD2 subsetD)
-*)
+
 
 declare [[ atp_problem_prefix = "Abstraction__CLF_eq_Collect_Pi" ]]
 lemma 
@@ -211,9 +161,7 @@
    CLF = (SIGMA cl: CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> 
    f \<in> pset cl \<rightarrow> pset cl"
 by auto
-(*??no longer terminates, with combinators
-by (metis Collect_mem_eq SigmaD2 contra_subsetD equalityE)
-*)
+
 
 declare [[ atp_problem_prefix = "Abstraction__CLF_eq_Collect_Pi_mono" ]]
 lemma 
@@ -225,37 +173,33 @@
 declare [[ atp_problem_prefix = "Abstraction__map_eq_zipA" ]]
 lemma "map (%x. (f x, g x)) xs = zip (map f xs) (map g xs)"
 apply (induct xs)
-(*sledgehammer*)  
-apply auto
-done
+ apply (metis map_is_Nil_conv zip.simps(1))
+by auto
 
 declare [[ atp_problem_prefix = "Abstraction__map_eq_zipB" ]]
 lemma "map (%w. (w -> w, w \<times> w)) xs = 
        zip (map (%w. w -> w) xs) (map (%w. w \<times> w) xs)"
 apply (induct xs)
-(*sledgehammer*)  
-apply auto
-done
+ apply (metis Nil_is_map_conv zip_Nil)
+by auto
 
 declare [[ atp_problem_prefix = "Abstraction__image_evenA" ]]
-lemma "(%x. Suc(f x)) ` {x. even x} <= A ==> (\<forall>x. even x --> Suc(f x) \<in> A)";
-(*sledgehammer*)  
-by auto
+lemma "(%x. Suc(f x)) ` {x. even x} <= A ==> (\<forall>x. even x --> Suc(f x) \<in> A)"
+by (metis Collect_def image_subset_iff mem_def)
 
 declare [[ atp_problem_prefix = "Abstraction__image_evenB" ]]
 lemma "(%x. f (f x)) ` ((%x. Suc(f x)) ` {x. even x}) <= A 
        ==> (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)";
-(*sledgehammer*)  
-by auto
+by (metis Collect_def imageI image_image image_subset_iff mem_def)
 
 declare [[ atp_problem_prefix = "Abstraction__image_curry" ]]
 lemma "f \<in> (%u v. b \<times> u \<times> v) ` A ==> \<forall>u v. P (b \<times> u \<times> v) ==> P(f y)" 
-(*sledgehammer*)  
+(*sledgehammer*)
 by auto
 
 declare [[ atp_problem_prefix = "Abstraction__image_TimesA" ]]
 lemma image_TimesA: "(%(x,y). (f x, g y)) ` (A \<times> B) = (f`A) \<times> (g`B)"
-(*sledgehammer*) 
+(*sledgehammer*)
 apply (rule equalityI)
 (***Even the two inclusions are far too difficult
 using [[ atp_problem_prefix = "Abstraction__image_TimesA_simpler"]]
@@ -283,15 +227,15 @@
 
 declare [[ atp_problem_prefix = "Abstraction__image_TimesB" ]]
 lemma image_TimesB:
-    "(%(x,y,z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f`A) \<times> (g`B) \<times> (h`C)" 
-(*sledgehammer*) 
+    "(%(x,y,z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f`A) \<times> (g`B) \<times> (h`C)"
+(*sledgehammer*)
 by force
 
 declare [[ atp_problem_prefix = "Abstraction__image_TimesC" ]]
 lemma image_TimesC:
     "(%(x,y). (x \<rightarrow> x, y \<times> y)) ` (A \<times> B) = 
      ((%x. x \<rightarrow> x) ` A) \<times> ((%y. y \<times> y) ` B)" 
-(*sledgehammer*) 
+(*sledgehammer*)
 by auto
 
 end
diff -r 2a9d0ec8c10d -r ed99188882b1 src/HOL/Metis_Examples/BT.thy
--- a/src/HOL/Metis_Examples/BT.thy	Fri Apr 30 13:47:39 2010 +0200
+++ b/src/HOL/Metis_Examples/BT.thy	Fri Apr 30 14:00:47 2010 +0200
@@ -133,7 +133,7 @@
 apply (rule ext) 
 apply (induct_tac y)
  apply (metis bt_map.simps(1))
-by (metis COMBI_def bt_map.simps(2))
+by (metis bt_map.simps(2))
 
 declare [[ atp_problem_prefix = "BT__bt_map_appnd" ]]
 
diff -r 2a9d0ec8c10d -r ed99188882b1 src/HOL/Metis_Examples/BigO.thy
--- a/src/HOL/Metis_Examples/BigO.thy	Fri Apr 30 13:47:39 2010 +0200
+++ b/src/HOL/Metis_Examples/BigO.thy	Fri Apr 30 14:00:47 2010 +0200
@@ -23,7 +23,7 @@
   apply (case_tac "c = 0", simp)
   apply (rule_tac x = "1" in exI, simp)
   apply (rule_tac x = "abs c" in exI, auto)
-  apply (metis abs_ge_minus_self abs_ge_zero abs_minus_cancel abs_of_nonneg equation_minus_iff Orderings.xt1(6) abs_mult)
+  apply (metis abs_ge_zero abs_of_nonneg Orderings.xt1(6) abs_mult)
   done
 
 (*** Now various verions with an increasing shrink factor ***)
@@ -37,64 +37,25 @@
   apply (case_tac "c = 0", simp)
   apply (rule_tac x = "1" in exI, simp)
   apply (rule_tac x = "abs c" in exI, auto)
-proof (neg_clausify)
-fix c x
-have 0: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom. \<bar>X1 * X2\<bar> = \<bar>X2 * X1\<bar>"
-  by (metis abs_mult mult_commute)
-have 1: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom.
-   X1 \<le> (0\<Colon>'a\<Colon>linordered_idom) \<or> \<bar>X2\<bar> * X1 = \<bar>X2 * X1\<bar>"
-  by (metis abs_mult_pos linorder_linear)
-have 2: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom.
-   \<not> (0\<Colon>'a\<Colon>linordered_idom) < X1 * X2 \<or>
-   \<not> (0\<Colon>'a\<Colon>linordered_idom) \<le> X2 \<or> \<not> X1 \<le> (0\<Colon>'a\<Colon>linordered_idom)"
-  by (metis linorder_not_less mult_nonneg_nonpos2)
-assume 3: "\<And>x\<Colon>'b\<Colon>type.
-   \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>
-   \<le> (c\<Colon>'a\<Colon>linordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
-assume 4: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
-  \<le> \<bar>c\<Colon>'a\<Colon>linordered_idom\<bar> * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
-have 5: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
-  \<le> \<bar>(c\<Colon>'a\<Colon>linordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
-  by (metis 4 abs_mult)
-have 6: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom.
-   \<not> X1 \<le> (0\<Colon>'a\<Colon>linordered_idom) \<or> X1 \<le> \<bar>X2\<bar>"
-  by (metis abs_ge_zero xt1(6))
-have 7: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom.
-   X1 \<le> \<bar>X2\<bar> \<or> (0\<Colon>'a\<Colon>linordered_idom) < X1"
-  by (metis not_leE 6)
-have 8: "(0\<Colon>'a\<Colon>linordered_idom) < \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>"
-  by (metis 5 7)
-have 9: "\<And>X1\<Colon>'a\<Colon>linordered_idom.
-   \<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar> \<le> X1 \<or>
-   (0\<Colon>'a\<Colon>linordered_idom) < X1"
-  by (metis 8 order_less_le_trans)
-have 10: "(0\<Colon>'a\<Colon>linordered_idom)
-< (c\<Colon>'a\<Colon>linordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>"
-  by (metis 3 9)
-have 11: "\<not> (c\<Colon>'a\<Colon>linordered_idom) \<le> (0\<Colon>'a\<Colon>linordered_idom)"
-  by (metis abs_ge_zero 2 10)
-have 12: "\<And>X1\<Colon>'a\<Colon>linordered_idom. (c\<Colon>'a\<Colon>linordered_idom) * \<bar>X1\<bar> = \<bar>X1 * c\<bar>"
-  by (metis mult_commute 1 11)
-have 13: "\<And>X1\<Colon>'b\<Colon>type.
-   - (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1
-   \<le> (c\<Colon>'a\<Colon>linordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1\<bar>"
-  by (metis 3 abs_le_D2)
-have 14: "\<And>X1\<Colon>'b\<Colon>type.
-   - (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1
-   \<le> \<bar>(c\<Colon>'a\<Colon>linordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1\<bar>"
-  by (metis 0 12 13)
-have 15: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom. \<bar>X1 * \<bar>X2\<bar>\<bar> = \<bar>X1 * X2\<bar>"
-  by (metis abs_mult abs_mult_pos abs_ge_zero)
-have 16: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom. X1 \<le> \<bar>X2\<bar> \<or> \<not> X1 \<le> X2"
-  by (metis xt1(6) abs_ge_self)
-have 17: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom. \<not> \<bar>X1\<bar> \<le> X2 \<or> X1 \<le> \<bar>X2\<bar>"
-  by (metis 16 abs_le_D1)
-have 18: "\<And>X1\<Colon>'b\<Colon>type.
-   (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1
-   \<le> \<bar>(c\<Colon>'a\<Colon>linordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1\<bar>"
-  by (metis 17 3 15)
-show "False"
-  by (metis abs_le_iff 5 18 14)
+proof -
+  fix c :: 'a and x :: 'b
+  assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
+  have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> \<bar>x\<^isub>1\<bar>" by (metis abs_ge_zero)
+  have F2: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1)
+  have F3: "\<forall>x\<^isub>1 x\<^isub>3. x\<^isub>3 \<le> \<bar>h x\<^isub>1\<bar> \<longrightarrow> x\<^isub>3 \<le> c * \<bar>f x\<^isub>1\<bar>" by (metis A1 order_trans)
+  have F4: "\<forall>x\<^isub>2 x\<^isub>3\<Colon>'a\<Colon>linordered_idom. \<bar>x\<^isub>3\<bar> * \<bar>x\<^isub>2\<bar> = \<bar>x\<^isub>3 * x\<^isub>2\<bar>"
+    by (metis abs_mult)
+  have F5: "\<forall>x\<^isub>3 x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> x\<^isub>1 \<longrightarrow> \<bar>x\<^isub>3 * x\<^isub>1\<bar> = \<bar>x\<^isub>3\<bar> * x\<^isub>1"
+    by (metis abs_mult_pos)
+  hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = \<bar>1\<bar> * x\<^isub>1" by (metis F2)
+  hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F2 abs_one)
+  hence "\<forall>x\<^isub>3. 0 \<le> \<bar>h x\<^isub>3\<bar> \<longrightarrow> \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>" by (metis F3)
+  hence "\<forall>x\<^isub>3. \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>" by (metis F1)
+  hence "\<forall>x\<^isub>3. (0\<Colon>'a) \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c\<bar> * \<bar>f x\<^isub>3\<bar>" by (metis F5)
+  hence "\<forall>x\<^isub>3. (0\<Colon>'a) \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c * f x\<^isub>3\<bar>" by (metis F4)
+  hence "\<forall>x\<^isub>3. c * \<bar>f x\<^isub>3\<bar> = \<bar>c * f x\<^isub>3\<bar>" by (metis F1)
+  hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1)
+  thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F4)
 qed
 
 sledgehammer_params [shrink_factor = 2]
@@ -106,36 +67,17 @@
   apply (case_tac "c = 0", simp)
   apply (rule_tac x = "1" in exI, simp)
   apply (rule_tac x = "abs c" in exI, auto);
-proof (neg_clausify)
-fix c x
-have 0: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom. \<bar>X1 * X2\<bar> = \<bar>X2 * X1\<bar>"
-  by (metis abs_mult mult_commute)
-assume 1: "\<And>x\<Colon>'b\<Colon>type.
-   \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>
-   \<le> (c\<Colon>'a\<Colon>linordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
-assume 2: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
-  \<le> \<bar>c\<Colon>'a\<Colon>linordered_idom\<bar> * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
-have 3: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
-  \<le> \<bar>(c\<Colon>'a\<Colon>linordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
-  by (metis 2 abs_mult)
-have 4: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom.
-   \<not> X1 \<le> (0\<Colon>'a\<Colon>linordered_idom) \<or> X1 \<le> \<bar>X2\<bar>"
-  by (metis abs_ge_zero xt1(6))
-have 5: "(0\<Colon>'a\<Colon>linordered_idom) < \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>"
-  by (metis not_leE 4 3)
-have 6: "(0\<Colon>'a\<Colon>linordered_idom)
-< (c\<Colon>'a\<Colon>linordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>"
-  by (metis 1 order_less_le_trans 5)
-have 7: "\<And>X1\<Colon>'a\<Colon>linordered_idom. (c\<Colon>'a\<Colon>linordered_idom) * \<bar>X1\<bar> = \<bar>X1 * c\<bar>"
-  by (metis abs_ge_zero linorder_not_less mult_nonneg_nonpos2 6 linorder_linear abs_mult_pos mult_commute)
-have 8: "\<And>X1\<Colon>'b\<Colon>type.
-   - (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1
-   \<le> \<bar>(c\<Colon>'a\<Colon>linordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1\<bar>"
-  by (metis 0 7 abs_le_D2 1)
-have 9: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom. \<not> \<bar>X1\<bar> \<le> X2 \<or> X1 \<le> \<bar>X2\<bar>"
-  by (metis abs_ge_self xt1(6) abs_le_D1)
-show "False"
-  by (metis 8 abs_ge_zero abs_mult_pos abs_mult 1 9 3 abs_le_iff)
+proof -
+  fix c :: 'a and x :: 'b
+  assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
+  have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1)
+  have F2: "\<forall>x\<^isub>2 x\<^isub>3\<Colon>'a\<Colon>linordered_idom. \<bar>x\<^isub>3\<bar> * \<bar>x\<^isub>2\<bar> = \<bar>x\<^isub>3 * x\<^isub>2\<bar>"
+    by (metis abs_mult)
+  have "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F1 abs_mult_pos abs_one)
+  hence "\<forall>x\<^isub>3. \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>" by (metis A1 abs_ge_zero order_trans)
+  hence "\<forall>x\<^isub>3. 0 \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c * f x\<^isub>3\<bar>" by (metis F2 abs_mult_pos)
+  hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1 abs_ge_zero)
+  thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis F2)
 qed
 
 sledgehammer_params [shrink_factor = 3]
@@ -146,30 +88,17 @@
   apply auto
   apply (case_tac "c = 0", simp)
   apply (rule_tac x = "1" in exI, simp)
-  apply (rule_tac x = "abs c" in exI, auto);
-proof (neg_clausify)
-fix c x
-assume 0: "\<And>x\<Colon>'b\<Colon>type.
-   \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>
-   \<le> (c\<Colon>'a\<Colon>linordered_idom) * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
-assume 1: "\<not> \<bar>(h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) (x\<Colon>'b\<Colon>type)\<bar>
-  \<le> \<bar>c\<Colon>'a\<Colon>linordered_idom\<bar> * \<bar>(f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) x\<bar>"
-have 2: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom.
-   X1 \<le> \<bar>X2\<bar> \<or> (0\<Colon>'a\<Colon>linordered_idom) < X1"
-  by (metis abs_ge_zero xt1(6) not_leE)
-have 3: "\<not> (c\<Colon>'a\<Colon>linordered_idom) \<le> (0\<Colon>'a\<Colon>linordered_idom)"
-  by (metis abs_ge_zero mult_nonneg_nonpos2 linorder_not_less order_less_le_trans 1 abs_mult 2 0)
-have 4: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2\<Colon>'a\<Colon>linordered_idom. \<bar>X1 * \<bar>X2\<bar>\<bar> = \<bar>X1 * X2\<bar>"
-  by (metis abs_ge_zero abs_mult_pos abs_mult)
-have 5: "\<And>X1\<Colon>'b\<Colon>type.
-   (h\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1
-   \<le> \<bar>(c\<Colon>'a\<Colon>linordered_idom) * (f\<Colon>'b\<Colon>type \<Rightarrow> 'a\<Colon>linordered_idom) X1\<bar>"
-  by (metis 4 0 xt1(6) abs_ge_self abs_le_D1)
-show "False"
-  by (metis abs_mult mult_commute 3 abs_mult_pos linorder_linear 0 abs_le_D2 5 1 abs_le_iff)
+  apply (rule_tac x = "abs c" in exI, auto)
+proof -
+  fix c :: 'a and x :: 'b
+  assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
+  have F1: "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1)
+  have F2: "\<forall>x\<^isub>3 x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 0 \<le> x\<^isub>1 \<longrightarrow> \<bar>x\<^isub>3 * x\<^isub>1\<bar> = \<bar>x\<^isub>3\<bar> * x\<^isub>1" by (metis abs_mult_pos)
+  hence "\<forall>x\<^isub>1\<ge>0. \<bar>x\<^isub>1\<Colon>'a\<Colon>linordered_idom\<bar> = x\<^isub>1" by (metis F1 abs_one)
+  hence "\<forall>x\<^isub>3. 0 \<le> \<bar>f x\<^isub>3\<bar> \<longrightarrow> c * \<bar>f x\<^isub>3\<bar> = \<bar>c\<bar> * \<bar>f x\<^isub>3\<bar>" by (metis F2 A1 abs_ge_zero order_trans)
+  thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis A1 abs_mult abs_ge_zero)
 qed
 
-
 sledgehammer_params [shrink_factor = 4]
 
 lemma (*bigo_pos_const:*) "(EX (c::'a::linordered_idom). 
@@ -178,33 +107,18 @@
   apply auto
   apply (case_tac "c = 0", simp)
   apply (rule_tac x = "1" in exI, simp)
-  apply (rule_tac x = "abs c" in exI, auto);
-proof (neg_clausify)
-fix c x  (*sort/type constraint inserted by hand!*)
-have 0: "\<And>(X1\<Colon>'a\<Colon>linordered_idom) X2. \<bar>X1 * \<bar>X2\<bar>\<bar> = \<bar>X1 * X2\<bar>"
-  by (metis abs_ge_zero abs_mult_pos abs_mult)
-assume 1: "\<And>A. \<bar>h A\<bar> \<le> c * \<bar>f A\<bar>"
-have 2: "\<And>X1 X2. \<not> \<bar>X1\<bar> \<le> X2 \<or> (0\<Colon>'a) \<le> X2"
-  by (metis abs_ge_zero order_trans)
-have 3: "\<And>X1. (0\<Colon>'a) \<le> c * \<bar>f X1\<bar>"
-  by (metis 1 2)
-have 4: "\<And>X1. c * \<bar>f X1\<bar> = \<bar>c * f X1\<bar>"
-  by (metis 0 abs_of_nonneg 3)
-have 5: "\<And>X1. - h X1 \<le> c * \<bar>f X1\<bar>"
-  by (metis 1 abs_le_D2)
-have 6: "\<And>X1. - h X1 \<le> \<bar>c * f X1\<bar>"
-  by (metis 4 5)
-have 7: "\<And>X1. h X1 \<le> c * \<bar>f X1\<bar>"
-  by (metis 1 abs_le_D1)
-have 8: "\<And>X1. h X1 \<le> \<bar>c * f X1\<bar>"
-  by (metis 4 7)
-assume 9: "\<not> \<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>"
-have 10: "\<not> \<bar>h x\<bar> \<le> \<bar>c * f x\<bar>"
-  by (metis abs_mult 9)
-show "False"
-  by (metis 6 8 10 abs_leI)
+  apply (rule_tac x = "abs c" in exI, auto)
+proof -
+  fix c :: 'a and x :: 'b
+  assume A1: "\<forall>x. \<bar>h x\<bar> \<le> c * \<bar>f x\<bar>"
+  have "\<forall>x\<^isub>1\<Colon>'a\<Colon>linordered_idom. 1 * x\<^isub>1 = x\<^isub>1" by (metis class_semiring.mul_1)
+  hence "\<forall>x\<^isub>3. \<bar>c * \<bar>f x\<^isub>3\<bar>\<bar> = c * \<bar>f x\<^isub>3\<bar>"
+    by (metis A1 abs_ge_zero order_trans abs_mult_pos abs_one)
+  hence "\<bar>h x\<bar> \<le> \<bar>c * f x\<bar>" by (metis A1 abs_ge_zero abs_mult_pos abs_mult)
+  thus "\<bar>h x\<bar> \<le> \<bar>c\<bar> * \<bar>f x\<bar>" by (metis abs_mult)
 qed
 
+sledgehammer_params [shrink_factor = 1]
 
 lemma bigo_alt_def: "O(f) = 
     {h. EX c. (0 < c & (ALL x. abs (h x) <= c * abs (f x)))}"
@@ -230,29 +144,13 @@
 
 declare [[ atp_problem_prefix = "BigO__bigo_refl" ]]
 lemma bigo_refl [intro]: "f : O(f)"
-  apply(auto simp add: bigo_def)
-proof (neg_clausify)
-fix x
-assume 0: "\<And>xa. \<not> \<bar>f (x xa)\<bar> \<le> xa * \<bar>f (x xa)\<bar>"
-have 1: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2 \<or> \<not> (1\<Colon>'b) \<le> (1\<Colon>'b)"
-  by (metis mult_le_cancel_right1 order_eq_iff)
-have 2: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2"
-  by (metis order_eq_iff 1)
-show "False"
-  by (metis 0 2)
-qed
+apply (auto simp add: bigo_def)
+by (metis class_semiring.mul_1 order_refl)
 
 declare [[ atp_problem_prefix = "BigO__bigo_zero" ]]
 lemma bigo_zero: "0 : O(g)"
-  apply (auto simp add: bigo_def func_zero)
-proof (neg_clausify)
-fix x
-assume 0: "\<And>xa. \<not> (0\<Colon>'b) \<le> xa * \<bar>g (x xa)\<bar>"
-have 1: "\<not> (0\<Colon>'b) \<le> (0\<Colon>'b)"
-  by (metis 0 mult_eq_0_iff)
-show "False"
-  by (metis 1 linorder_neq_iff linorder_antisym_conv1)
-qed
+apply (auto simp add: bigo_def func_zero)
+by (metis class_semiring.mul_0 order_refl)
 
 lemma bigo_zero2: "O(%x.0) = {%x.0}"
   apply (auto simp add: bigo_def) 
@@ -365,103 +263,36 @@
 lemma bigo_bounded_alt: "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> 
     f : O(g)" 
   apply (auto simp add: bigo_def)
-(*Version 1: one-shot proof*)
+(* Version 1: one-line proof *)
   apply (metis abs_le_D1 linorder_class.not_less  order_less_le  Orderings.xt1(12)  abs_mult)
   done
 
 lemma (*bigo_bounded_alt:*) "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> 
-    f : O(g)" 
-  apply (auto simp add: bigo_def)
-(*Version 2: single-step proof*)
-proof (neg_clausify)
-fix x
-assume 0: "\<And>x. f x \<le> c * g x"
-assume 1: "\<And>xa. \<not> f (x xa) \<le> xa * \<bar>g (x xa)\<bar>"
-have 2: "\<And>X3. c * g X3 = f X3 \<or> \<not> c * g X3 \<le> f X3"
-  by (metis 0 order_antisym_conv)
-have 3: "\<And>X3. \<not> f (x \<bar>X3\<bar>) \<le> \<bar>X3 * g (x \<bar>X3\<bar>)\<bar>"
-  by (metis 1 abs_mult)
-have 4: "\<And>X1 X3\<Colon>'b\<Colon>linordered_idom. X3 \<le> X1 \<or> X1 \<le> \<bar>X3\<bar>"
-  by (metis linorder_linear abs_le_D1)
-have 5: "\<And>X3::'b. \<bar>X3\<bar> * \<bar>X3\<bar> = X3 * X3"
-  by (metis abs_mult_self)
-have 6: "\<And>X3. \<not> X3 * X3 < (0\<Colon>'b\<Colon>linordered_idom)"
-  by (metis not_square_less_zero)
-have 7: "\<And>X1 X3::'b. \<bar>X1\<bar> * \<bar>X3\<bar> = \<bar>X3 * X1\<bar>"
-  by (metis abs_mult mult_commute)
-have 8: "\<And>X3::'b. X3 * X3 = \<bar>X3 * X3\<bar>"
-  by (metis abs_mult 5)
-have 9: "\<And>X3. X3 * g (x \<bar>X3\<bar>) \<le> f (x \<bar>X3\<bar>)"
-  by (metis 3 4)
-have 10: "c * g (x \<bar>c\<bar>) = f (x \<bar>c\<bar>)"
-  by (metis 2 9)
-have 11: "\<And>X3::'b. \<bar>X3\<bar> * \<bar>\<bar>X3\<bar>\<bar> = \<bar>X3\<bar> * \<bar>X3\<bar>"
-  by (metis abs_idempotent abs_mult 8)
-have 12: "\<And>X3::'b. \<bar>X3 * \<bar>X3\<bar>\<bar> = \<bar>X3\<bar> * \<bar>X3\<bar>"
-  by (metis mult_commute 7 11)
-have 13: "\<And>X3::'b. \<bar>X3 * \<bar>X3\<bar>\<bar> = X3 * X3"
-  by (metis 8 7 12)
-have 14: "\<And>X3. X3 \<le> \<bar>X3\<bar> \<or> X3 < (0\<Colon>'b)"
-  by (metis abs_ge_self abs_le_D1 abs_if)
-have 15: "\<And>X3. X3 \<le> \<bar>X3\<bar> \<or> \<bar>X3\<bar> < (0\<Colon>'b)"
-  by (metis abs_ge_self abs_le_D1 abs_if)
-have 16: "\<And>X3. X3 * X3 < (0\<Colon>'b) \<or> X3 * \<bar>X3\<bar> \<le> X3 * X3"
-  by (metis 15 13)
-have 17: "\<And>X3::'b. X3 * \<bar>X3\<bar> \<le> X3 * X3"
-  by (metis 16 6)
-have 18: "\<And>X3. X3 \<le> \<bar>X3\<bar> \<or> \<not> X3 < (0\<Colon>'b)"
-  by (metis mult_le_cancel_left 17)
-have 19: "\<And>X3::'b. X3 \<le> \<bar>X3\<bar>"
-  by (metis 18 14)
-have 20: "\<not> f (x \<bar>c\<bar>) \<le> \<bar>f (x \<bar>c\<bar>)\<bar>"
-  by (metis 3 10)
-show "False"
-  by (metis 20 19)
+    f : O(g)"
+apply (auto simp add: bigo_def)
+(* Version 2: structured proof *)
+proof -
+  assume "\<forall>x. f x \<le> c * g x"
+  thus "\<exists>c. \<forall>x. f x \<le> c * \<bar>g x\<bar>" by (metis abs_mult abs_ge_self order_trans)
 qed
 
+text{*So here is the easier (and more natural) problem using transitivity*}
+declare [[ atp_problem_prefix = "BigO__bigo_bounded_alt_trans" ]]
+lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)" 
+apply (auto simp add: bigo_def)
+(* Version 1: one-line proof *)
+by (metis abs_ge_self abs_mult order_trans)
 
 text{*So here is the easier (and more natural) problem using transitivity*}
 declare [[ atp_problem_prefix = "BigO__bigo_bounded_alt_trans" ]]
 lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)" 
   apply (auto simp add: bigo_def)
-  (*Version 1: one-shot proof*) 
-  apply (metis Orderings.leD Orderings.leI abs_ge_self abs_le_D1 abs_mult abs_of_nonneg order_le_less)
-  done
-
-text{*So here is the easier (and more natural) problem using transitivity*}
-declare [[ atp_problem_prefix = "BigO__bigo_bounded_alt_trans" ]]
-lemma "ALL x. 0 <= f x ==> ALL x. f x <= c * g x ==> f : O(g)" 
-  apply (auto simp add: bigo_def)
-(*Version 2: single-step proof*)
-proof (neg_clausify)
-fix x
-assume 0: "\<And>A\<Colon>'a\<Colon>type.
-   (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) A
-   \<le> (c\<Colon>'b\<Colon>linordered_idom) * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) A"
-assume 1: "\<And>A\<Colon>'b\<Colon>linordered_idom.
-   \<not> (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) ((x\<Colon>'b\<Colon>linordered_idom \<Rightarrow> 'a\<Colon>type) A)
-     \<le> A * \<bar>(g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) (x A)\<bar>"
-have 2: "\<And>X2\<Colon>'a\<Colon>type.
-   \<not> (c\<Colon>'b\<Colon>linordered_idom) * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) X2
-     < (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) X2"
-  by (metis 0 linorder_not_le)
-have 3: "\<And>X2\<Colon>'b\<Colon>linordered_idom.
-   \<not> (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) ((x\<Colon>'b\<Colon>linordered_idom \<Rightarrow> 'a\<Colon>type) \<bar>X2\<bar>)
-     \<le> \<bar>X2 * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) (x \<bar>X2\<bar>)\<bar>"
-  by (metis abs_mult 1)
-have 4: "\<And>X2\<Colon>'b\<Colon>linordered_idom.
-   \<bar>X2 * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) ((x\<Colon>'b\<Colon>linordered_idom \<Rightarrow> 'a\<Colon>type) \<bar>X2\<bar>)\<bar>
-   < (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) (x \<bar>X2\<bar>)"
-  by (metis 3 linorder_not_less)
-have 5: "\<And>X2\<Colon>'b\<Colon>linordered_idom.
-   X2 * (g\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) ((x\<Colon>'b\<Colon>linordered_idom \<Rightarrow> 'a\<Colon>type) \<bar>X2\<bar>)
-   < (f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) (x \<bar>X2\<bar>)"
-  by (metis abs_less_iff 4)
-show "False"
-  by (metis 2 5)
+(* Version 2: structured proof *)
+proof -
+  assume "\<forall>x. f x \<le> c * g x"
+  thus "\<exists>c. \<forall>x. f x \<le> c * \<bar>g x\<bar>" by (metis abs_mult abs_ge_self order_trans)
 qed
 
-
 lemma bigo_bounded: "ALL x. 0 <= f x ==> ALL x. f x <= g x ==> 
     f : O(g)" 
   apply (erule bigo_bounded_alt [of f 1 g])
@@ -471,63 +302,37 @@
 declare [[ atp_problem_prefix = "BigO__bigo_bounded2" ]]
 lemma bigo_bounded2: "ALL x. lb x <= f x ==> ALL x. f x <= lb x + g x ==>
     f : lb +o O(g)"
-  apply (rule set_minus_imp_plus)
-  apply (rule bigo_bounded)
-  apply (auto simp add: diff_minus fun_Compl_def func_plus)
-  prefer 2
-  apply (drule_tac x = x in spec)+ 
-  apply arith (*not clear that it's provable otherwise*) 
-proof (neg_clausify)
-fix x
-assume 0: "\<And>y. lb y \<le> f y"
-assume 1: "\<not> (0\<Colon>'b) \<le> f x + - lb x"
-have 2: "\<And>X3. (0\<Colon>'b) + X3 = X3"
-  by (metis diff_eq_eq right_minus_eq)
-have 3: "\<not> (0\<Colon>'b) \<le> f x - lb x"
-  by (metis 1 diff_minus)
-have 4: "\<not> (0\<Colon>'b) + lb x \<le> f x"
-  by (metis 3 le_diff_eq)
-show "False"
-  by (metis 4 2 0)
+apply (rule set_minus_imp_plus)
+apply (rule bigo_bounded)
+ apply (auto simp add: diff_minus fun_Compl_def func_plus)
+ prefer 2
+ apply (drule_tac x = x in spec)+
+ apply (metis add_right_mono class_semiring.semiring_rules(24) diff_add_cancel diff_minus_eq_add le_less order_trans)
+proof -
+  fix x :: 'a
+  assume "\<forall>x. lb x \<le> f x"
+  thus "(0\<Colon>'b) \<le> f x + - lb x" by (metis not_leE diff_minus less_iff_diff_less_0 less_le_not_le)
 qed
 
 declare [[ atp_problem_prefix = "BigO__bigo_abs" ]]
 lemma bigo_abs: "(%x. abs(f x)) =o O(f)" 
-  apply (unfold bigo_def)
-  apply auto
-proof (neg_clausify)
-fix x
-assume 0: "\<And>xa. \<not> \<bar>f (x xa)\<bar> \<le> xa * \<bar>f (x xa)\<bar>"
-have 1: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2 \<or> \<not> (1\<Colon>'b) \<le> (1\<Colon>'b)"
-  by (metis mult_le_cancel_right1 order_eq_iff)
-have 2: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2"
-  by (metis order_eq_iff 1)
-show "False"
-  by (metis 0 2)
-qed
+apply (unfold bigo_def)
+apply auto
+by (metis class_semiring.mul_1 order_refl)
 
 declare [[ atp_problem_prefix = "BigO__bigo_abs2" ]]
 lemma bigo_abs2: "f =o O(%x. abs(f x))"
-  apply (unfold bigo_def)
-  apply auto
-proof (neg_clausify)
-fix x
-assume 0: "\<And>xa. \<not> \<bar>f (x xa)\<bar> \<le> xa * \<bar>f (x xa)\<bar>"
-have 1: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2 \<or> \<not> (1\<Colon>'b) \<le> (1\<Colon>'b)"
-  by (metis mult_le_cancel_right1 order_eq_iff)
-have 2: "\<And>X2. X2 \<le> (1\<Colon>'b) * X2"
-  by (metis order_eq_iff 1)
-show "False"
-  by (metis 0 2)
-qed
+apply (unfold bigo_def)
+apply auto
+by (metis class_semiring.mul_1 order_refl)
  
 lemma bigo_abs3: "O(f) = O(%x. abs(f x))"
-  apply (rule equalityI)
-  apply (rule bigo_elt_subset)
-  apply (rule bigo_abs2)
-  apply (rule bigo_elt_subset)
-  apply (rule bigo_abs)
-done
+proof -
+  have F1: "\<forall>v u. u \<in> O(v) \<longrightarrow> O(u) \<subseteq> O(v)" by (metis bigo_elt_subset)
+  have F2: "\<forall>u. (\<lambda>R. \<bar>u R\<bar>) \<in> O(u)" by (metis bigo_abs)
+  have "\<forall>u. u \<in> O(\<lambda>R. \<bar>u R\<bar>)" by (metis bigo_abs2)
+  thus "O(f) = O(\<lambda>x. \<bar>f x\<bar>)" using F1 F2 by auto
+qed 
 
 lemma bigo_abs4: "f =o g +o O(h) ==> 
     (%x. abs (f x)) =o (%x. abs (g x)) +o O(h)"
@@ -597,63 +402,9 @@
   abs_mult mult_pos_pos)
   apply (erule ssubst) 
   apply (subst abs_mult)
-(*not qute BigO__bigo_mult_simpler_1 (a hard problem!) as abs_mult has
-  just been done*)
-proof (neg_clausify)
-fix a c b ca x
-assume 0: "(0\<Colon>'b\<Colon>linordered_idom) < (c\<Colon>'b\<Colon>linordered_idom)"
-assume 1: "\<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar>
-\<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>"
-assume 2: "\<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar>
-\<le> (ca\<Colon>'b\<Colon>linordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>"
-assume 3: "\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar> *
-  \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>
-  \<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> *
-    ((ca\<Colon>'b\<Colon>linordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>)"
-have 4: "\<bar>c\<Colon>'b\<Colon>linordered_idom\<bar> = c"
-  by (metis abs_of_pos 0)
-have 5: "\<And>X1\<Colon>'b\<Colon>linordered_idom. (c\<Colon>'b\<Colon>linordered_idom) * \<bar>X1\<bar> = \<bar>c * X1\<bar>"
-  by (metis abs_mult 4)
-have 6: "(0\<Colon>'b\<Colon>linordered_idom) = (1\<Colon>'b\<Colon>linordered_idom) \<or>
-(0\<Colon>'b\<Colon>linordered_idom) < (1\<Colon>'b\<Colon>linordered_idom)"
-  by (metis abs_not_less_zero abs_one linorder_neqE_linordered_idom)
-have 7: "(0\<Colon>'b\<Colon>linordered_idom) < (1\<Colon>'b\<Colon>linordered_idom)"
-  by (metis 6 one_neq_zero)
-have 8: "\<bar>1\<Colon>'b\<Colon>linordered_idom\<bar> = (1\<Colon>'b\<Colon>linordered_idom)"
-  by (metis abs_of_pos 7)
-have 9: "\<And>X1\<Colon>'b\<Colon>linordered_idom. (0\<Colon>'b\<Colon>linordered_idom) \<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>X1\<bar>"
-  by (metis abs_ge_zero 5)
-have 10: "\<And>X1\<Colon>'b\<Colon>linordered_idom. X1 * (1\<Colon>'b\<Colon>linordered_idom) = X1"
-  by (metis mult_cancel_right2 mult_commute)
-have 11: "\<And>X1\<Colon>'b\<Colon>linordered_idom. \<bar>\<bar>X1\<bar>\<bar> = \<bar>X1\<bar> * \<bar>1\<Colon>'b\<Colon>linordered_idom\<bar>"
-  by (metis abs_mult abs_idempotent 10)
-have 12: "\<And>X1\<Colon>'b\<Colon>linordered_idom. \<bar>\<bar>X1\<bar>\<bar> = \<bar>X1\<bar>"
-  by (metis 11 8 10)
-have 13: "\<And>X1\<Colon>'b\<Colon>linordered_idom. (0\<Colon>'b\<Colon>linordered_idom) \<le> \<bar>X1\<bar>"
-  by (metis abs_ge_zero 12)
-have 14: "\<not> (0\<Colon>'b\<Colon>linordered_idom)
-  \<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar> \<or>
-\<not> (0\<Colon>'b\<Colon>linordered_idom) \<le> \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> \<or>
-\<not> \<bar>b x\<bar> \<le> (ca\<Colon>'b\<Colon>linordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> \<or>
-\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> \<le> c * \<bar>f x\<bar>"
-  by (metis 3 mult_mono)
-have 15: "\<not> (0\<Colon>'b\<Colon>linordered_idom) \<le> \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar> \<or>
-\<not> \<bar>b x\<bar> \<le> (ca\<Colon>'b\<Colon>linordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> \<or>
-\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>
-  \<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>"
-  by (metis 14 9)
-have 16: "\<not> \<bar>(b\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar>
-  \<le> (ca\<Colon>'b\<Colon>linordered_idom) * \<bar>(g\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar> \<or>
-\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>
-  \<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>"
-  by (metis 15 13)
-have 17: "\<not> \<bar>(a\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) (x\<Colon>'a)\<bar>
-  \<le> (c\<Colon>'b\<Colon>linordered_idom) * \<bar>(f\<Colon>'a \<Rightarrow> 'b\<Colon>linordered_idom) x\<bar>"
-  by (metis 16 2)
-show 18: "False"
-  by (metis 17 1)
-qed
-
+(* not quite as hard as BigO__bigo_mult_simpler_1 (a hard problem!) since
+   abs_mult has just been done *)
+by (metis abs_ge_zero mult_mono')
 
 declare [[ atp_problem_prefix = "BigO__bigo_mult2" ]]
 lemma bigo_mult2 [intro]: "f *o O(g) <= O(f * g)"
@@ -672,7 +423,7 @@
 
 declare [[ atp_problem_prefix = "BigO__bigo_mult3" ]]
 lemma bigo_mult3: "f : O(h) ==> g : O(j) ==> f * g : O(h * j)"
-by (metis bigo_mult set_times_intro subset_iff)
+by (metis bigo_mult set_rev_mp set_times_intro)
 
 declare [[ atp_problem_prefix = "BigO__bigo_mult4" ]]
 lemma bigo_mult4 [intro]:"f : k +o O(h) ==> g * f : (g * k) +o O(g * h)"
@@ -809,40 +560,16 @@
 by (metis bigo_const1 bigo_elt_subset);
 
 lemma bigo_const2 [intro]: "O(%x. c::'b::linordered_idom) <= O(%x. 1)";
-(*??FAILS because the two occurrences of COMBK have different polymorphic types
-proof (neg_clausify)
-assume 0: "\<not> O(COMBK (c\<Colon>'b\<Colon>linordered_idom)) \<subseteq> O(COMBK (1\<Colon>'b\<Colon>linordered_idom))"
-have 1: "COMBK (c\<Colon>'b\<Colon>linordered_idom) \<notin> O(COMBK (1\<Colon>'b\<Colon>linordered_idom))"
-apply (rule notI) 
-apply (rule 0 [THEN notE]) 
-apply (rule bigo_elt_subset) 
-apply assumption; 
-sorry
-  by (metis 0 bigo_elt_subset)  loops??
-show "False"
-  by (metis 1 bigo_const1)
+(* "thus" had to be replaced by "show" with an explicit reference to "F1" *)
+proof -
+  have F1: "\<forall>u. (\<lambda>Q. u) \<in> O(\<lambda>Q. 1)" by (metis bigo_const1)
+  show "O(\<lambda>x. c) \<subseteq> O(\<lambda>x. 1)" by (metis F1 bigo_elt_subset)
 qed
-*)
-  apply (rule bigo_elt_subset)
-  apply (rule bigo_const1)
-done
 
 declare [[ atp_problem_prefix = "BigO__bigo_const3" ]]
 lemma bigo_const3: "(c::'a::linordered_field) ~= 0 ==> (%x. 1) : O(%x. c)"
 apply (simp add: bigo_def)
-proof (neg_clausify)
-assume 0: "(c\<Colon>'a\<Colon>linordered_field) \<noteq> (0\<Colon>'a\<Colon>linordered_field)"
-assume 1: "\<And>A\<Colon>'a\<Colon>linordered_field. \<not> (1\<Colon>'a\<Colon>linordered_field) \<le> A * \<bar>c\<Colon>'a\<Colon>linordered_field\<bar>"
-have 2: "(0\<Colon>'a\<Colon>linordered_field) = \<bar>c\<Colon>'a\<Colon>linordered_field\<bar> \<or>
-\<not> (1\<Colon>'a\<Colon>linordered_field) \<le> (1\<Colon>'a\<Colon>linordered_field)"
-  by (metis 1 field_inverse)
-have 3: "\<bar>c\<Colon>'a\<Colon>linordered_field\<bar> = (0\<Colon>'a\<Colon>linordered_field)"
-  by (metis linorder_neq_iff linorder_antisym_conv1 2)
-have 4: "(0\<Colon>'a\<Colon>linordered_field) = (c\<Colon>'a\<Colon>linordered_field)"
-  by (metis 3 abs_eq_0)
-show "False"
-  by (metis 0 4)
-qed
+by (metis abs_eq_0 left_inverse order_refl)
 
 lemma bigo_const4: "(c::'a::linordered_field) ~= 0 ==> O(%x. 1) <= O(%x. c)"
 by (rule bigo_elt_subset, rule bigo_const3, assumption)
@@ -854,15 +581,7 @@
 declare [[ atp_problem_prefix = "BigO__bigo_const_mult1" ]]
 lemma bigo_const_mult1: "(%x. c * f x) : O(f)"
   apply (simp add: bigo_def abs_mult)
-proof (neg_clausify)
-fix x
-assume 0: "\<And>xa\<Colon>'b\<Colon>linordered_idom.
-   \<not> \<bar>c\<Colon>'b\<Colon>linordered_idom\<bar> *
-     \<bar>(f\<Colon>'a\<Colon>type \<Rightarrow> 'b\<Colon>linordered_idom) ((x\<Colon>'b\<Colon>linordered_idom \<Rightarrow> 'a\<Colon>type) xa)\<bar>
-     \<le> xa * \<bar>f (x xa)\<bar>"
-show "False"
-  by (metis linorder_neq_iff linorder_antisym_conv1 0)
-qed
+by (metis le_less)
 
 lemma bigo_const_mult2: "O(%x. c * f x) <= O(f)"
 by (rule bigo_elt_subset, rule bigo_const_mult1)
@@ -870,7 +589,7 @@
 declare [[ atp_problem_prefix = "BigO__bigo_const_mult3" ]]
 lemma bigo_const_mult3: "(c::'a::linordered_field) ~= 0 ==> f : O(%x. c * f x)"
   apply (simp add: bigo_def)
-(*sledgehammer [no luck]*); 
+(*sledgehammer [no luck]*)
   apply (rule_tac x = "abs(inverse c)" in exI)
   apply (simp only: abs_mult [symmetric] mult_assoc [symmetric])
 apply (subst left_inverse) 
@@ -1132,15 +851,17 @@
 
 declare [[ atp_problem_prefix = "BigO__bigo_lesso1" ]]
 lemma bigo_lesso1: "ALL x. f x <= g x ==> f <o g =o O(h)"
-  apply (unfold lesso_def)
-  apply (subgoal_tac "(%x. max (f x - g x) 0) = 0")
-(*??Translation of TSTP raised an exception: Type unification failed: Variable ?'X2.0::type not of sort ord*)
-apply (metis bigo_zero)
+apply (unfold lesso_def)
+apply (subgoal_tac "(%x. max (f x - g x) 0) = 0")
+proof -
+  assume "(\<lambda>x. max (f x - g x) 0) = 0"
+  thus "(\<lambda>x. max (f x - g x) 0) \<in> O(h)" by (metis bigo_zero)
+next
+  show "\<forall>x\<Colon>'a. f x \<le> g x \<Longrightarrow> (\<lambda>x\<Colon>'a. max (f x - g x) (0\<Colon>'b)) = (0\<Colon>'a \<Rightarrow> 'b)"
   apply (unfold func_zero)
   apply (rule ext)
-  apply (simp split: split_max)
-done
-
+  by (simp split: split_max)
+qed
 
 declare [[ atp_problem_prefix = "BigO__bigo_lesso2" ]]
 lemma bigo_lesso2: "f =o g +o O(h) ==>
@@ -1156,8 +877,9 @@
 apply (erule thin_rl)
 (*sledgehammer*);  
   apply (case_tac "0 <= k x - g x")
-  prefer 2 (*re-order subgoals because I don't know what to put after a structured proof*)
-   apply (metis abs_ge_zero abs_minus_commute linorder_linear min_max.sup_absorb1 min_max.sup_commute)
+(* apply (metis abs_le_iff add_le_imp_le_right diff_minus le_less
+                le_max_iff_disj min_max.le_supE min_max.sup_absorb2
+                min_max.sup_commute) *)
 proof (neg_clausify)
 fix x
 assume 0: "\<And>A. k A \<le> f A"
@@ -1177,6 +899,11 @@
   by (metis 5 abs_minus_commute 7 min_max.sup_commute 6)
 show "False"
   by (metis min_max.sup_commute min_max.inf_commute min_max.sup_inf_absorb min_max.le_iff_inf 0 max_diff_distrib_left 1 linorder_not_le 8)
+next
+  show "\<And>x\<Colon>'a.
+       \<lbrakk>\<forall>x\<Colon>'a. (0\<Colon>'b) \<le> k x; \<forall>x\<Colon>'a. k x \<le> f x; \<not> (0\<Colon>'b) \<le> k x - g x\<rbrakk>
+       \<Longrightarrow> max (k x - g x) (0\<Colon>'b) \<le> \<bar>f x - g x\<bar>"
+    by (metis abs_ge_zero le_cases min_max.sup_absorb2)
 qed
 
 declare [[ atp_problem_prefix = "BigO__bigo_lesso3" ]]
diff -r 2a9d0ec8c10d -r ed99188882b1 src/HOL/Metis_Examples/Message.thy
--- a/src/HOL/Metis_Examples/Message.thy	Fri Apr 30 13:47:39 2010 +0200
+++ b/src/HOL/Metis_Examples/Message.thy	Fri Apr 30 14:00:47 2010 +0200
@@ -4,11 +4,12 @@
 Testing the metis method.
 *)
 
-theory Message imports Main begin
+theory Message
+imports Main
+begin
 
-(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
 lemma strange_Un_eq [simp]: "A \<union> (B \<union> A) = B \<union> A"
-by blast
+by (metis Un_ac(2) Un_ac(3))
 
 types 
   key = nat
@@ -20,7 +21,7 @@
 specification (invKey)
   invKey [simp]: "invKey (invKey K) = K"
   invKey_symmetric: "all_symmetric --> invKey = id"
-    by (rule exI [of _ id], auto)
+by (metis id_apply)
 
 
 text{*The inverse of a symmetric key is itself; that of a public key
@@ -74,33 +75,28 @@
   | Snd:         "{|X,Y|}   \<in> parts H ==> Y \<in> parts H"
   | Body:        "Crypt K X \<in> parts H ==> X \<in> parts H"
 
-
-declare [[ atp_problem_prefix = "Message__parts_mono" ]]
 lemma parts_mono: "G \<subseteq> H ==> parts(G) \<subseteq> parts(H)"
 apply auto
-apply (erule parts.induct) 
-apply (metis Inj set_mp)
-apply (metis Fst)
-apply (metis Snd)
-apply (metis Body)
-done
-
+apply (erule parts.induct)
+   apply (metis parts.Inj set_rev_mp)
+  apply (metis parts.Fst)
+ apply (metis parts.Snd)
+by (metis parts.Body)
 
 text{*Equations hold because constructors are injective.*}
 lemma Friend_image_eq [simp]: "(Friend x \<in> Friend`A) = (x:A)"
-by auto
+by (metis agent.inject imageI image_iff)
 
-lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x\<in>A)"
-by auto
+lemma Key_image_eq [simp]: "(Key x \<in> Key`A) = (x \<in> A)"
+by (metis image_iff msg.inject(4))
 
-lemma Nonce_Key_image_eq [simp]: "(Nonce x \<notin> Key`A)"
-by auto
+lemma Nonce_Key_image_eq [simp]: "Nonce x \<notin> Key`A"
+by (metis image_iff msg.distinct(23))
 
 
 subsubsection{*Inverse of keys *}
 
-declare [[ atp_problem_prefix = "Message__invKey_eq" ]]
-lemma invKey_eq [simp]: "(invKey K = invKey K') = (K=K')"
+lemma invKey_eq [simp]: "(invKey K = invKey K') = (K = K')"
 by (metis invKey)
 
 
@@ -155,7 +151,7 @@
          [| X \<in> parts H; Y \<in> parts H |] ==> P |] ==> P"
 by (blast dest: parts.Fst parts.Snd) 
 
-    declare MPair_parts [elim!]  parts.Body [dest!]
+declare MPair_parts [elim!] parts.Body [dest!]
 text{*NB These two rules are UNSAFE in the formal sense, as they discard the
      compound message.  They work well on THIS FILE.  
   @{text MPair_parts} is left as SAFE because it speeds up proofs.
@@ -200,7 +196,6 @@
 apply (simp only: parts_Un)
 done
 
-declare [[ atp_problem_prefix = "Message__parts_insert_two" ]]
 lemma parts_insert2:
      "parts (insert X (insert Y H)) = parts {X} \<union> parts {Y} \<union> parts H"
 by (metis Un_commute Un_empty_left Un_empty_right Un_insert_left Un_insert_right parts_Un)
@@ -237,7 +232,6 @@
 lemma parts_idem [simp]: "parts (parts H) = parts H"
 by blast
 
-declare [[ atp_problem_prefix = "Message__parts_subset_iff" ]]
 lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) = (G \<subseteq> parts H)"
 apply (rule iffI) 
 apply (metis Un_absorb1 Un_subset_iff parts_Un parts_increasing)
@@ -247,13 +241,10 @@
 lemma parts_trans: "[| X\<in> parts G;  G \<subseteq> parts H |] ==> X\<in> parts H"
 by (blast dest: parts_mono); 
 
-
-declare [[ atp_problem_prefix = "Message__parts_cut" ]]
 lemma parts_cut: "[|Y\<in> parts(insert X G);  X\<in> parts H|] ==> Y\<in> parts(G \<union> H)"
 by (metis Un_insert_left Un_insert_right insert_absorb mem_def parts_Un parts_idem sup1CI)
 
 
-
 subsubsection{*Rewrite rules for pulling out atomic messages *}
 
 lemmas parts_insert_eq_I = equalityI [OF subsetI parts_insert_subset]
@@ -312,8 +303,6 @@
 apply (erule parts.induct, auto)
 done
 
-
-declare [[ atp_problem_prefix = "Message__msg_Nonce_supply" ]]
 lemma msg_Nonce_supply: "\<exists>N. \<forall>n. N\<le>n --> Nonce n \<notin> parts {msg}"
 apply (induct_tac "msg") 
 apply (simp_all add: parts_insert2)
@@ -364,8 +353,6 @@
 
 lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
 
-
-declare [[ atp_problem_prefix = "Message__parts_analz" ]]
 lemma parts_analz [simp]: "parts (analz H) = parts H"
 apply (rule equalityI)
 apply (metis analz_subset_parts parts_subset_iff)
@@ -517,8 +504,8 @@
 by (drule analz_mono, blast)
 
 
-declare [[ atp_problem_prefix = "Message__analz_cut" ]]
-    declare analz_trans[intro]
+declare analz_trans[intro]
+
 lemma analz_cut: "[| Y\<in> analz (insert X H);  X\<in> analz H |] ==> Y\<in> analz H"
 (*TOO SLOW
 by (metis analz_idem analz_increasing analz_mono insert_absorb insert_mono insert_subset) --{*317s*}
@@ -535,7 +522,6 @@
 
 text{*A congruence rule for "analz" *}
 
-declare [[ atp_problem_prefix = "Message__analz_subset_cong" ]]
 lemma analz_subset_cong:
      "[| analz G \<subseteq> analz G'; analz H \<subseteq> analz H' |] 
       ==> analz (G \<union> H) \<subseteq> analz (G' \<union> H')"
@@ -612,9 +598,6 @@
 lemma synth_Un: "synth(G) \<union> synth(H) \<subseteq> synth(G \<union> H)"
 by (intro Un_least synth_mono Un_upper1 Un_upper2)
 
-
-declare [[ atp_problem_prefix = "Message__synth_insert" ]]
- 
 lemma synth_insert: "insert X (synth H) \<subseteq> synth(insert X H)"
 by (metis insert_iff insert_subset subset_insertI synth.Inj synth_mono)
 
@@ -635,7 +618,6 @@
 lemma synth_trans: "[| X\<in> synth G;  G \<subseteq> synth H |] ==> X\<in> synth H"
 by (drule synth_mono, blast)
 
-declare [[ atp_problem_prefix = "Message__synth_cut" ]]
 lemma synth_cut: "[| Y\<in> synth (insert X H);  X\<in> synth H |] ==> Y\<in> synth H"
 (*TOO SLOW
 by (metis insert_absorb insert_mono insert_subset synth_idem synth_increasing synth_mono)
@@ -667,7 +649,6 @@
 
 subsubsection{*Combinations of parts, analz and synth *}
 
-declare [[ atp_problem_prefix = "Message__parts_synth" ]]
 lemma parts_synth [simp]: "parts (synth H) = parts H \<union> synth H"
 apply (rule equalityI)
 apply (rule subsetI)
@@ -679,18 +660,14 @@
 apply (metis Un_subset_iff parts_increasing parts_mono synth_increasing)
 done
 
-
-
-
-declare [[ atp_problem_prefix = "Message__analz_analz_Un" ]]
 lemma analz_analz_Un [simp]: "analz (analz G \<union> H) = analz (G \<union> H)"
 apply (rule equalityI);
 apply (metis analz_idem analz_subset_cong order_eq_refl)
 apply (metis analz_increasing analz_subset_cong order_eq_refl)
 done
 
-declare [[ atp_problem_prefix = "Message__analz_synth_Un" ]]
-    declare analz_mono [intro] analz.Fst [intro] analz.Snd [intro] Un_least [intro]
+declare analz_mono [intro] analz.Fst [intro] analz.Snd [intro] Un_least [intro]
+
 lemma analz_synth_Un [simp]: "analz (synth G \<union> H) = analz (G \<union> H) \<union> synth G"
 apply (rule equalityI)
 apply (rule subsetI)
@@ -702,102 +679,81 @@
 apply blast
 done
 
-declare [[ atp_problem_prefix = "Message__analz_synth" ]]
 lemma analz_synth [simp]: "analz (synth H) = analz H \<union> synth H"
-proof (neg_clausify)
-assume 0: "analz (synth H) \<noteq> analz H \<union> synth H"
-have 1: "\<And>X1 X3. sup (analz (sup X3 X1)) (synth X3) = analz (sup (synth X3) X1)"
-  by (metis analz_synth_Un)
-have 2: "sup (analz H) (synth H) \<noteq> analz (synth H)"
-  by (metis 0)
-have 3: "\<And>X1 X3. sup (synth X3) (analz (sup X3 X1)) = analz (sup (synth X3) X1)"
-  by (metis 1 Un_commute)
-have 4: "\<And>X3. sup (synth X3) (analz X3) = analz (sup (synth X3) {})"
-  by (metis 3 Un_empty_right)
-have 5: "\<And>X3. sup (synth X3) (analz X3) = analz (synth X3)"
-  by (metis 4 Un_empty_right)
-have 6: "\<And>X3. sup (analz X3) (synth X3) = analz (synth X3)"
-  by (metis 5 Un_commute)
-show "False"
-  by (metis 2 6)
+proof -
+  have "\<forall>x\<^isub>2 x\<^isub>1. synth x\<^isub>1 \<union> analz (x\<^isub>1 \<union> x\<^isub>2) = analz (synth x\<^isub>1 \<union> x\<^isub>2)"
+    by (metis Un_commute analz_synth_Un)
+  hence "\<forall>x\<^isub>3 x\<^isub>1. synth x\<^isub>1 \<union> analz x\<^isub>1 = analz (synth x\<^isub>1 \<union> UNION {} x\<^isub>3)"
+    by (metis UN_extend_simps(3))
+  hence "\<forall>x\<^isub>1. synth x\<^isub>1 \<union> analz x\<^isub>1 = analz (synth x\<^isub>1)"
+    by (metis UN_extend_simps(3))
+  hence "\<forall>x\<^isub>1. analz x\<^isub>1 \<union> synth x\<^isub>1 = analz (synth x\<^isub>1)"
+    by (metis Un_commute)
+  thus "analz (synth H) = analz H \<union> synth H" by metis
 qed
 
 
 subsubsection{*For reasoning about the Fake rule in traces *}
 
-declare [[ atp_problem_prefix = "Message__parts_insert_subset_Un" ]]
 lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
-proof (neg_clausify)
-assume 0: "X \<in> G"
-assume 1: "\<not> parts (insert X H) \<subseteq> parts G \<union> parts H"
-have 2: "\<not> parts (insert X H) \<subseteq> parts (G \<union> H)"
-  by (metis 1 parts_Un)
-have 3: "\<not> insert X H \<subseteq> G \<union> H"
-  by (metis 2 parts_mono)
-have 4: "X \<notin> G \<union> H \<or> \<not> H \<subseteq> G \<union> H"
-  by (metis 3 insert_subset)
-have 5: "X \<notin> G \<union> H"
-  by (metis 4 Un_upper2)
-have 6: "X \<notin> G"
-  by (metis 5 UnCI)
-show "False"
-  by (metis 6 0)
+proof -
+  assume "X \<in> G"
+  hence "\<forall>u. X \<in> G \<union> u" by (metis Un_iff)
+  hence "X \<in> G \<union> H \<and> H \<subseteq> G \<union> H"
+    by (metis Un_upper2)
+  hence "insert X H \<subseteq> G \<union> H" by (metis insert_subset)
+  hence "parts (insert X H) \<subseteq> parts (G \<union> H)"
+    by (metis parts_mono)
+  thus "parts (insert X H) \<subseteq> parts G \<union> parts H"
+    by (metis parts_Un)
 qed
 
-declare [[ atp_problem_prefix = "Message__Fake_parts_insert" ]]
 lemma Fake_parts_insert:
      "X \<in> synth (analz H) ==>  
       parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
-proof (neg_clausify)
-assume 0: "X \<in> synth (analz H)"
-assume 1: "\<not> parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
-have 2: "\<And>X3. parts X3 \<union> synth (analz X3) = parts (synth (analz X3))"
-  by (metis parts_synth parts_analz)
-have 3: "\<And>X3. analz X3 \<union> synth (analz X3) = analz (synth (analz X3))"
-  by (metis analz_synth analz_idem)
-have 4: "\<And>X3. analz X3 \<subseteq> analz (synth X3)"
-  by (metis Un_upper1 analz_synth)
-have 5: "\<not> parts (insert X H) \<subseteq> parts H \<union> synth (analz H)"
-  by (metis 1 Un_commute)
-have 6: "\<not> parts (insert X H) \<subseteq> parts (synth (analz H))"
-  by (metis 5 2)
-have 7: "\<not> insert X H \<subseteq> synth (analz H)"
-  by (metis 6 parts_mono)
-have 8: "X \<notin> synth (analz H) \<or> \<not> H \<subseteq> synth (analz H)"
-  by (metis 7 insert_subset)
-have 9: "\<not> H \<subseteq> synth (analz H)"
-  by (metis 8 0)
-have 10: "\<And>X3. X3 \<subseteq> analz (synth X3)"
-  by (metis analz_subset_iff 4)
-have 11: "\<And>X3. X3 \<subseteq> analz (synth (analz X3))"
-  by (metis analz_subset_iff 10)
-have 12: "\<And>X3. analz (synth (analz X3)) = synth (analz X3) \<or>
-     \<not> analz X3 \<subseteq> synth (analz X3)"
-  by (metis Un_absorb1 3)
-have 13: "\<And>X3. analz (synth (analz X3)) = synth (analz X3)"
-  by (metis 12 synth_increasing)
-have 14: "\<And>X3. X3 \<subseteq> synth (analz X3)"
-  by (metis 11 13)
-show "False"
-  by (metis 9 14)
+sledgehammer
+proof -
+  assume A1: "X \<in> synth (analz H)"
+  have F1: "\<forall>x\<^isub>1. analz x\<^isub>1 \<union> synth (analz x\<^isub>1) = analz (synth (analz x\<^isub>1))"
+    by (metis analz_idem analz_synth)
+  have F2: "\<forall>x\<^isub>1. parts x\<^isub>1 \<union> synth (analz x\<^isub>1) = parts (synth (analz x\<^isub>1))"
+    by (metis parts_analz parts_synth)
+  have F3: "synth (analz H) X" using A1 by (metis mem_def)
+  have "\<forall>x\<^isub>2 x\<^isub>1\<Colon>msg set. x\<^isub>1 \<le> sup x\<^isub>1 x\<^isub>2" by (metis inf_sup_ord(3))
+  hence F4: "\<forall>x\<^isub>1. analz x\<^isub>1 \<subseteq> analz (synth x\<^isub>1)" by (metis analz_synth)
+  have F5: "X \<in> synth (analz H)" using F3 by (metis mem_def)
+  have "\<forall>x\<^isub>1. analz x\<^isub>1 \<subseteq> synth (analz x\<^isub>1)
+         \<longrightarrow> analz (synth (analz x\<^isub>1)) = synth (analz x\<^isub>1)"
+    using F1 by (metis subset_Un_eq)
+  hence F6: "\<forall>x\<^isub>1. analz (synth (analz x\<^isub>1)) = synth (analz x\<^isub>1)"
+    by (metis synth_increasing)
+  have "\<forall>x\<^isub>1. x\<^isub>1 \<subseteq> analz (synth x\<^isub>1)" using F4 by (metis analz_subset_iff)
+  hence "\<forall>x\<^isub>1. x\<^isub>1 \<subseteq> analz (synth (analz x\<^isub>1))" by (metis analz_subset_iff)
+  hence "\<forall>x\<^isub>1. x\<^isub>1 \<subseteq> synth (analz x\<^isub>1)" using F6 by metis
+  hence "H \<subseteq> synth (analz H)" by metis
+  hence "H \<subseteq> synth (analz H) \<and> X \<in> synth (analz H)" using F5 by metis
+  hence "insert X H \<subseteq> synth (analz H)" by (metis insert_subset)
+  hence "parts (insert X H) \<subseteq> parts (synth (analz H))" by (metis parts_mono)
+  hence "parts (insert X H) \<subseteq> parts H \<union> synth (analz H)" using F2 by metis
+  thus "parts (insert X H) \<subseteq> synth (analz H) \<union> parts H" by (metis Un_commute)
 qed
 
 lemma Fake_parts_insert_in_Un:
      "[|Z \<in> parts (insert X H);  X: synth (analz H)|] 
       ==> Z \<in>  synth (analz H) \<union> parts H";
-by (blast dest: Fake_parts_insert  [THEN subsetD, dest])
+by (blast dest: Fake_parts_insert [THEN subsetD, dest])
 
-declare [[ atp_problem_prefix = "Message__Fake_analz_insert" ]]
-    declare analz_mono [intro] synth_mono [intro] 
+declare analz_mono [intro] synth_mono [intro] 
+
 lemma Fake_analz_insert:
-     "X\<in> synth (analz G) ==>  
+     "X \<in> synth (analz G) ==>
       analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
-by (metis Un_commute Un_insert_left Un_insert_right Un_upper1 analz_analz_Un analz_mono analz_synth_Un equalityE insert_absorb order_le_less xt1(12))
+by (metis Un_commute Un_insert_left Un_insert_right Un_upper1 analz_analz_Un
+          analz_mono analz_synth_Un insert_absorb)
 
-declare [[ atp_problem_prefix = "Message__Fake_analz_insert_simpler" ]]
-(*simpler problems?  BUT METIS CAN'T PROVE
+(* Simpler problems?  BUT METIS CAN'T PROVE THE LAST STEP
 lemma Fake_analz_insert_simpler:
-     "X\<in> synth (analz G) ==>  
+     "X \<in> synth (analz G) ==>  
       analz (insert X H) \<subseteq> synth (analz G) \<union> analz (G \<union> H)"
 apply (rule subsetI)
 apply (subgoal_tac "x \<in> analz (synth (analz G) \<union> H) ")
diff -r 2a9d0ec8c10d -r ed99188882b1 src/HOL/Metis_Examples/Tarski.thy
--- a/src/HOL/Metis_Examples/Tarski.thy	Fri Apr 30 13:47:39 2010 +0200
+++ b/src/HOL/Metis_Examples/Tarski.thy	Fri Apr 30 14:00:47 2010 +0200
@@ -514,67 +514,44 @@
      "H = {x. (x, f x) \<in> r & x \<in> A} ==> lub H cl \<in> fix f A"
 apply (simp add: fix_def)
 apply (rule conjI)
-proof (neg_clausify)
-assume 0: "H =
-Collect
- (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r)) (COMBC op \<in> A))"
-assume 1: "lub (Collect
-      (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r))
-        (COMBC op \<in> A)))
- cl
-\<notin> A"
-have 2: "lub H cl \<notin> A"
-  by (metis 1 0)
-have 3: "(lub H cl, f (lub H cl)) \<in> r"
-  by (metis lubH_le_flubH 0)
-have 4: "(f (lub H cl), lub H cl) \<in> r"
-  by (metis flubH_le_lubH 0)
-have 5: "lub H cl = f (lub H cl) \<or> (lub H cl, f (lub H cl)) \<notin> r"
-  by (metis antisymE 4)
-have 6: "lub H cl = f (lub H cl)"
-  by (metis 5 3)
-have 7: "(lub H cl, lub H cl) \<in> r"
-  by (metis 6 4)
-have 8: "\<And>X1. lub H cl \<in> X1 \<or> \<not> refl_on X1 r"
-  by (metis 7 refl_onD2)
-have 9: "\<not> refl_on A r"
-  by (metis 8 2)
-show "False"
-  by (metis CO_refl_on 9);
-next --{*apparently the way to insert a second structured proof*}
-  show "H = {x. (x, f x) \<in> r \<and> x \<in> A} \<Longrightarrow>
-  f (lub {x. (x, f x) \<in> r \<and> x \<in> A} cl) = lub {x. (x, f x) \<in> r \<and> x \<in> A} cl"
-  proof (neg_clausify)
-  assume 0: "H =
-  Collect
-   (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r)) (COMBC op \<in> A))"
-  assume 1: "f (lub (Collect
-           (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r))
-             (COMBC op \<in> A)))
-      cl) \<noteq>
-  lub (Collect
-        (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r))
-          (COMBC op \<in> A)))
-   cl"
-  have 2: "f (lub H cl) \<noteq>
-  lub (Collect
-        (COMBS (COMBB op \<and> (COMBC (COMBB op \<in> (COMBS Pair f)) r))
-          (COMBC op \<in> A)))
-   cl"
-    by (metis 1 0)
-  have 3: "f (lub H cl) \<noteq> lub H cl"
-    by (metis 2 0)
-  have 4: "(lub H cl, f (lub H cl)) \<in> r"
-    by (metis lubH_le_flubH 0)
-  have 5: "(f (lub H cl), lub H cl) \<in> r"
-    by (metis flubH_le_lubH 0)
-  have 6: "lub H cl = f (lub H cl) \<or> (lub H cl, f (lub H cl)) \<notin> r"
-    by (metis antisymE 5)
-  have 7: "lub H cl = f (lub H cl)"
-    by (metis 6 4)
-  show "False"
-    by (metis 3 7)
-  qed
+proof -
+  assume A1: "H = {x. (x, f x) \<in> r \<and> x \<in> A}"
+  have F1: "\<forall>x\<^isub>2. (\<lambda>R. R \<in> x\<^isub>2) = x\<^isub>2" by (metis Collect_def Collect_mem_eq)
+  have F2: "\<forall>x\<^isub>1 x\<^isub>2. (\<lambda>R. x\<^isub>2 (x\<^isub>1 R)) = x\<^isub>1 -` x\<^isub>2"
+    by (metis Collect_def vimage_Collect_eq)
+  have F3: "\<forall>x\<^isub>2 x\<^isub>1. (\<lambda>R. x\<^isub>1 R \<in> x\<^isub>2) = x\<^isub>1 -` x\<^isub>2"
+    by (metis Collect_def vimage_def)
+  have F4: "\<forall>x\<^isub>3 x\<^isub>1. (\<lambda>R. x\<^isub>1 R \<and> x\<^isub>3 R) = x\<^isub>1 \<inter> x\<^isub>3"
+    by (metis Collect_def Collect_conj_eq)
+  have F5: "(\<lambda>R. (R, f R) \<in> r \<and> R \<in> A) = H" using A1 by (metis Collect_def)
+  have F6: "\<forall>x\<^isub>1\<subseteq>A. glb x\<^isub>1 (dual cl) \<in> A" by (metis lub_dual_glb lub_in_lattice)
+  have F7: "\<forall>x\<^isub>2 x\<^isub>1. (\<lambda>R. x\<^isub>1 R \<in> x\<^isub>2) = (\<lambda>R. x\<^isub>2 (x\<^isub>1 R))" by (metis F2 F3)
+  have "(\<lambda>R. (R, f R) \<in> r \<and> A R) = H" by (metis F1 F5)
+  hence "A \<inter> (\<lambda>R. r (R, f R)) = H" by (metis F4 F7 Int_commute)
+  hence "H \<subseteq> A" by (metis Int_lower1)
+  hence "H \<subseteq> A" by metis
+  hence "glb H (dual cl) \<in> A" using F6 by metis
+  hence "glb (\<lambda>R. (R, f R) \<in> r \<and> R \<in> A) (dual cl) \<in> A" using F5 by metis
+  hence "lub (\<lambda>R. (R, f R) \<in> r \<and> R \<in> A) cl \<in> A" by (metis lub_dual_glb)
+  thus "lub {x. (x, f x) \<in> r \<and> x \<in> A} cl \<in> A" by (metis Collect_def)
+next
+  assume A1: "H = {x. (x, f x) \<in> r \<and> x \<in> A}"
+  have F1: "\<forall>v. (\<lambda>R. R \<in> v) = v" by (metis Collect_mem_eq Collect_def)
+  have F2: "\<forall>w u. (\<lambda>R. u R \<and> w R) = u \<inter> w"
+    by (metis Collect_conj_eq Collect_def)
+  have F3: "\<forall>x v. (\<lambda>R. v R \<in> x) = v -` x" by (metis vimage_def Collect_def)
+  hence F4: "A \<inter> (\<lambda>R. (R, f R)) -` r = H" using A1 by auto
+  hence F5: "(f (lub H cl), lub H cl) \<in> r"
+    by (metis F1 F3 F2 Int_commute flubH_le_lubH Collect_def)
+  have F6: "(lub H cl, f (lub H cl)) \<in> r"
+    by (metis F1 F3 F2 F4 Int_commute lubH_le_flubH Collect_def)
+  have "(lub H cl, f (lub H cl)) \<in> r \<longrightarrow> f (lub H cl) = lub H cl"
+    using F5 by (metis antisymE)
+  hence "f (lub H cl) = lub H cl" using F6 by metis
+  thus "H = {x. (x, f x) \<in> r \<and> x \<in> A}
+        \<Longrightarrow> f (lub {x. (x, f x) \<in> r \<and> x \<in> A} cl) =
+           lub {x. (x, f x) \<in> r \<and> x \<in> A} cl"
+    by (metis F4 F2 F3 F1 Collect_def Int_commute)
 qed
 
 lemma (in CLF) (*lubH_is_fixp:*)
@@ -744,18 +721,13 @@
      "[| a \<in> A; b \<in> A; interval r a b \<noteq> {} |]
       ==> (| pset = interval r a b, order = induced (interval r a b) r |)
           \<in> PartialOrder"
-proof (neg_clausify)
-assume 0: "a \<in> A"
-assume 1: "b \<in> A"
-assume 2: "\<lparr>pset = interval r a b, order = induced (interval r a b) r\<rparr> \<notin> PartialOrder"
-have 3: "\<not> interval r a b \<subseteq> A"
-  by (metis 2 po_subset_po)
-have 4: "b \<notin> A \<or> a \<notin> A"
-  by (metis 3 interval_subset)
-have 5: "a \<notin> A"
-  by (metis 4 1)
-show "False"
-  by (metis 5 0)
+proof -
+  assume A1: "a \<in> A"
+  assume "b \<in> A"
+  hence "\<forall>u. u \<in> A \<longrightarrow> interval r u b \<subseteq> A" by (metis interval_subset)
+  hence "interval r a b \<subseteq> A" using A1 by metis
+  hence "interval r a b \<subseteq> A" by metis
+  thus ?thesis by (metis po_subset_po)
 qed
 
 lemma (in CLF) intv_CL_lub:
@@ -1096,9 +1068,9 @@
 apply (blast intro!: Tarski.tarski_full_lemma [OF Tarski.intro, OF CLF.intro Tarski_axioms.intro,
   OF CL.intro CLF_axioms.intro, OF PO.intro CL_axioms.intro] cl_po cl_co f_cl)
 done
-  declare (in CLF) fixf_po[rule del] P_def [simp del] A_def [simp del] r_def [simp del]
+
+declare (in CLF) fixf_po [rule del] P_def [simp del] A_def [simp del] r_def [simp del]
          Tarski.tarski_full_lemma [rule del] cl_po [rule del] cl_co [rule del]
          CompleteLatticeI_simp [rule del]
 
-
 end
diff -r 2a9d0ec8c10d -r ed99188882b1 src/HOL/Metis_Examples/set.thy
--- a/src/HOL/Metis_Examples/set.thy	Fri Apr 30 13:47:39 2010 +0200
+++ b/src/HOL/Metis_Examples/set.thy	Fri Apr 30 14:00:47 2010 +0200
@@ -8,24 +8,21 @@
 imports Main
 begin
 
+sledgehammer_params [isar_proof, debug, overlord]
+
 lemma "EX x X. ALL y. EX z Z. (~P(y,y) | P(x,x) | ~S(z,x)) &
                (S(x,y) | ~S(y,z) | Q(Z,Z))  &
                (Q(X,y) | ~Q(y,Z) | S(X,X))" 
 by metis
-(*??But metis can't prove the single-step version...*)
-
-
 
 lemma "P(n::nat) ==> ~P(0) ==> n ~= 0"
 by metis
 
 sledgehammer_params [shrink_factor = 1]
 
-
 (*multiple versions of this example*)
 lemma (*equal_union: *)
-   "(X = Y \<union> Z) =
-    (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
+   "(X = Y \<union> Z) = (Y \<subseteq> X \<and> Z \<subseteq> X \<and> (\<forall>V. Y \<subseteq> V \<and> Z \<subseteq> V \<longrightarrow> X \<subseteq> V))"
 proof (neg_clausify)
 fix x
 assume 0: "Y \<subseteq> X \<or> X = Y \<union> Z"
@@ -269,15 +266,14 @@
       "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
       "P (f b) \<Longrightarrow> \<exists>s A. (\<forall>x \<in> A. P x) \<and> f s \<in> A"
       "\<exists>A. a \<notin> A"
-      "(\<forall>C. (0, 0) \<in> C \<and> (\<forall>x y. (x, y) \<in> C \<longrightarrow> (Suc x, Suc y) \<in> C) \<longrightarrow> (n, m) \<in> C) \<and> Q n \<longrightarrow> Q m" 
-apply (metis atMost_iff)
-apply (metis emptyE)
-apply (metis insert_iff singletonE)
+      "(\<forall>C. (0, 0) \<in> C \<and> (\<forall>x y. (x, y) \<in> C \<longrightarrow> (Suc x, Suc y) \<in> C) \<longrightarrow> (n, m) \<in> C) \<and> Q n \<longrightarrow> Q m"
+apply (metis all_not_in_conv)+
+apply (metis mem_def)
 apply (metis insertCI singletonE zless_le)
 apply (metis Collect_def Collect_mem_eq)
 apply (metis Collect_def Collect_mem_eq)
 apply (metis DiffE)
-apply (metis pair_in_Id_conv) 
+apply (metis pair_in_Id_conv)
 done
 
 end
diff -r 2a9d0ec8c10d -r ed99188882b1 src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Fri Apr 30 13:47:39 2010 +0200
+++ b/src/HOL/Sledgehammer.thy	Fri Apr 30 14:00:47 2010 +0200
@@ -25,28 +25,28 @@
   ("Tools/Sledgehammer/metis_tactics.ML")
 begin
 
-definition COMBI :: "'a \<Rightarrow> 'a"
-  where "COMBI P \<equiv> P"
+definition COMBI :: "'a \<Rightarrow> 'a" where
+[no_atp]: "COMBI P \<equiv> P"
 
-definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a"
-  where "COMBK P Q \<equiv> P"
+definition COMBK :: "'a \<Rightarrow> 'b \<Rightarrow> 'a" where
+[no_atp]: "COMBK P Q \<equiv> P"
 
-definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c"
-  where "COMBB P Q R \<equiv> P (Q R)"
+definition COMBB :: "('b => 'c) \<Rightarrow> ('a => 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where [no_atp]:
+"COMBB P Q R \<equiv> P (Q R)"
 
-definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c"
-  where "COMBC P Q R \<equiv> P R Q"
+definition COMBC :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
+[no_atp]: "COMBC P Q R \<equiv> P R Q"
 
-definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"
-  where "COMBS P Q R \<equiv> P R (Q R)"
+definition COMBS :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" where
+[no_atp]: "COMBS P Q R \<equiv> P R (Q R)"
 
-definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-  where "fequal X Y \<equiv> (X = Y)"
+definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where [no_atp]:
+"fequal X Y \<equiv> (X = Y)"
 
-lemma fequal_imp_equal: "fequal X Y \<Longrightarrow> X = Y"
+lemma fequal_imp_equal [no_atp]: "fequal X Y \<Longrightarrow> X = Y"
   by (simp add: fequal_def)
 
-lemma equal_imp_fequal: "X = Y \<Longrightarrow> fequal X Y"
+lemma equal_imp_fequal [no_atp]: "X = Y \<Longrightarrow> fequal X Y"
   by (simp add: fequal_def)
 
 text{*These two represent the equivalence between Boolean equality and iff.
@@ -61,31 +61,31 @@
 
 text{*Theorems for translation to combinators*}
 
-lemma abs_S: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
+lemma abs_S [no_atp]: "\<lambda>x. (f x) (g x) \<equiv> COMBS f g"
 apply (rule eq_reflection)
 apply (rule ext) 
 apply (simp add: COMBS_def) 
 done
 
-lemma abs_I: "\<lambda>x. x \<equiv> COMBI"
+lemma abs_I [no_atp]: "\<lambda>x. x \<equiv> COMBI"
 apply (rule eq_reflection)
 apply (rule ext) 
 apply (simp add: COMBI_def) 
 done
 
-lemma abs_K: "\<lambda>x. y \<equiv> COMBK y"
+lemma abs_K [no_atp]: "\<lambda>x. y \<equiv> COMBK y"
 apply (rule eq_reflection)
 apply (rule ext) 
 apply (simp add: COMBK_def) 
 done
 
-lemma abs_B: "\<lambda>x. a (g x) \<equiv> COMBB a g"
+lemma abs_B [no_atp]: "\<lambda>x. a (g x) \<equiv> COMBB a g"
 apply (rule eq_reflection)
 apply (rule ext) 
 apply (simp add: COMBB_def) 
 done
 
-lemma abs_C: "\<lambda>x. (f x) b \<equiv> COMBC f b"
+lemma abs_C [no_atp]: "\<lambda>x. (f x) b \<equiv> COMBC f b"
 apply (rule eq_reflection)
 apply (rule ext) 
 apply (simp add: COMBC_def) 
diff -r 2a9d0ec8c10d -r ed99188882b1 src/HOL/Tools/ATP_Manager/atp_systems.ML
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Fri Apr 30 13:47:39 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Fri Apr 30 14:00:47 2010 +0200
@@ -70,8 +70,10 @@
   case pairself (find_first (fn s => String.isSubstring s output))
                 (ListPair.unzip delims) of
     (SOME begin_delim, SOME end_delim) =>
-    output |> first_field begin_delim |> the |> snd
-           |> first_field end_delim |> the |> fst
+    (output |> first_field begin_delim |> the |> snd
+            |> first_field end_delim |> the |> fst
+            |> first_field "\n" |> the |> snd
+     handle Option.Option => "")
   | _ => ""
 
 fun extract_proof_and_outcome res_code proof_delims known_failures output =
@@ -139,8 +141,8 @@
     fun prob_pathname nr =
       let
         val probfile =
-          Path.basic (the_problem_prefix ^
-                      (if overlord then "_" ^ name else serial_string ())
+          Path.basic ((if overlord then "prob_" ^ name
+                       else the_problem_prefix ^ serial_string ())
                       ^ "_" ^ string_of_int nr)
       in
         if the_dest_dir = "" then File.tmp_path probfile
@@ -260,8 +262,10 @@
    arguments = fn timeout =>
      "--output_syntax tptp --mode casc -t " ^
      string_of_int (to_generous_secs timeout),
-   proof_delims = [("=========== Refutation ==========",
-                    "======= End of refutation =======")],
+   proof_delims =
+     [("=========== Refutation ==========",
+       "======= End of refutation ======="),
+      ("% SZS output start Refutation", "% SZS output end Refutation")],
    known_failures =
      [(Unprovable, "Satisfiability detected"),
       (OutOfResources, "CANNOT PROVE"),
diff -r 2a9d0ec8c10d -r ed99188882b1 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Apr 30 13:47:39 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Apr 30 14:00:47 2010 +0200
@@ -1260,15 +1260,15 @@
   | t1 $ _ => term_under_def t1
   | _ => t
 
-(* Here we crucially rely on "Refute.specialize_type" performing a preorder
-   traversal of the term, without which the wrong occurrence of a constant could
-   be matched in the face of overloading. *)
+(* Here we crucially rely on "specialize_type" performing a preorder traversal
+   of the term, without which the wrong occurrence of a constant could be
+   matched in the face of overloading. *)
 fun def_props_for_const thy stds fast_descrs table (x as (s, _)) =
   if is_built_in_const thy stds fast_descrs x then
     []
   else
     these (Symtab.lookup table s)
-    |> map_filter (try (Refute.specialize_type thy x))
+    |> map_filter (try (specialize_type thy x))
     |> filter (curry (op =) (Const x) o term_under_def)
 
 fun normalized_rhs_of t =
@@ -1381,8 +1381,8 @@
     SOME t' => is_constr_pattern_lhs thy t'
   | NONE => false
 
-(* Similar to "Refute.specialize_type" but returns all matches rather than only
-   the first (preorder) match. *)
+(* Similar to "specialize_type" but returns all matches rather than only the
+   first (preorder) match. *)
 fun multi_specialize_type thy slack (s, T) t =
   let
     fun aux (Const (s', T')) ys =
@@ -1390,8 +1390,8 @@
           ys |> (if AList.defined (op =) ys T' then
                    I
                  else
-                   cons (T', Refute.monomorphic_term
-                                 (Sign.typ_match thy (T', T) Vartab.empty) t)
+                   cons (T', monomorphic_term (Sign.typ_match thy (T', T)
+                                                              Vartab.empty) t)
                    handle Type.TYPE_MATCH => I
                         | Refute.REFUTE _ =>
                           if slack then
@@ -1682,7 +1682,7 @@
   let val abs_T = domain_type T in
     typedef_info thy (fst (dest_Type abs_T)) |> the
     |> pairf #Abs_inverse #Rep_inverse
-    |> pairself (Refute.specialize_type thy x o prop_of o the)
+    |> pairself (specialize_type thy x o prop_of o the)
     ||> single |> op ::
   end
 fun optimized_typedef_axioms thy (abs_z as (abs_s, _)) =
@@ -1697,7 +1697,7 @@
         val set_t = Const (set_name, rep_T --> bool_T)
         val set_t' =
           prop_of_Rep |> HOLogic.dest_Trueprop
-                      |> Refute.specialize_type thy (dest_Const rep_t)
+                      |> specialize_type thy (dest_Const rep_t)
                       |> HOLogic.dest_mem |> snd
       in
         [HOLogic.all_const abs_T
diff -r 2a9d0ec8c10d -r ed99188882b1 src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Apr 30 13:47:39 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Apr 30 14:00:47 2010 +0200
@@ -914,8 +914,8 @@
                  val class = Logic.class_of_const s
                  val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]),
                                                    class)
-                 val ax1 = try (Refute.specialize_type thy x) of_class
-                 val ax2 = Option.map (Refute.specialize_type thy x o snd)
+                 val ax1 = try (specialize_type thy x) of_class
+                 val ax2 = Option.map (specialize_type thy x o snd)
                                       (Refute.get_classdef thy class)
                in
                  fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
@@ -997,7 +997,7 @@
           map (fn t => case Term.add_tvars t [] of
                          [] => t
                        | [(x, S)] =>
-                         Refute.monomorphic_term (Vartab.make [(x, (S, T))]) t
+                         monomorphic_term (Vartab.make [(x, (S, T))]) t
                        | _ => raise TERM ("Nitpick_Preproc.axioms_for_term.\
                                           \add_axioms_for_sort", [t]))
               class_axioms
diff -r 2a9d0ec8c10d -r ed99188882b1 src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri Apr 30 13:47:39 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri Apr 30 14:00:47 2010 +0200
@@ -57,6 +57,8 @@
   val bool_T : typ
   val nat_T : typ
   val int_T : typ
+  val monomorphic_term : Type.tyenv -> term -> term
+  val specialize_type : theory -> (string * typ) -> term -> term
   val nat_subscript : int -> string
   val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
   val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
@@ -227,6 +229,9 @@
 val nat_T = @{typ nat}
 val int_T = @{typ int}
 
+val monomorphic_term = Sledgehammer_Util.monomorphic_term
+val specialize_type = Sledgehammer_Util.specialize_type
+
 val subscript = implode o map (prefix "\<^isub>") o explode
 fun nat_subscript n =
   (* cheap trick to ensure proper alphanumeric ordering for one- and two-digit
diff -r 2a9d0ec8c10d -r ed99188882b1 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Apr 30 13:47:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Fri Apr 30 14:00:47 2010 +0200
@@ -123,14 +123,16 @@
       in  (map (hol_literal_to_fol mode) lits, types_sorts) end;
 
 (*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
-fun metis_of_typeLit pos (LTVar (s,x))  = metis_lit pos s [Metis.Term.Var x]
-  | metis_of_typeLit pos (LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
+fun metis_of_type_literals pos (TyLitVar (s, (s', _))) =
+    metis_lit pos s [Metis.Term.Var s']
+  | metis_of_type_literals pos (TyLitFree (s, (s', _))) =
+    metis_lit pos s [Metis.Term.Fn (s',[])]
 
 fun default_sort _ (TVar _) = false
   | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
 
 fun metis_of_tfree tf =
-  Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit true tf));
+  Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_type_literals true tf));
 
 fun hol_thm_to_fol is_conjecture ctxt mode th =
   let val thy = ProofContext.theory_of ctxt
@@ -138,11 +140,12 @@
              (literals_of_hol_thm thy mode o HOLogic.dest_Trueprop o prop_of) th
   in
       if is_conjecture then
-          (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), add_typs types_sorts)
+          (Metis.Thm.axiom (Metis.LiteralSet.fromList mlits),
+           add_type_literals types_sorts)
       else
-        let val tylits = add_typs (filter (not o default_sort ctxt) types_sorts)
+        let val tylits = add_type_literals (filter (not o default_sort ctxt) types_sorts)
             val mtylits = if Config.get ctxt type_lits
-                          then map (metis_of_typeLit false) tylits else []
+                          then map (metis_of_type_literals false) tylits else []
         in
           (Metis.Thm.axiom (Metis.LiteralSet.fromList(mtylits @ mlits)), [])
         end
@@ -598,7 +601,9 @@
 (*Extract TFree constraints from context to include as conjecture clauses*)
 fun init_tfrees ctxt =
   let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts
-  in  add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
+  in
+    add_type_literals (Vartab.fold add (#2 (Variable.constraints_of ctxt)) [])
+  end;
 
 (*transform isabelle type / arity clause to metis clause *)
 fun add_type_thm [] lmap = lmap
@@ -669,7 +674,7 @@
       val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths
       val _ = if null tfrees then ()
               else (trace_msg (fn () => "TFREE CLAUSES");
-                    app (fn tf => trace_msg (fn _ => tptp_of_typeLit true tf)) tfrees)
+                    app (fn tf => trace_msg (fn _ => tptp_of_type_literal true tf NONE |> fst)) tfrees)
       val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
       val thms = map #1 axioms
       val _ = app (fn th => trace_msg (fn () => Metis.Thm.toString th)) thms
diff -r 2a9d0ec8c10d -r ed99188882b1 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Apr 30 13:47:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Fri Apr 30 14:00:47 2010 +0200
@@ -392,13 +392,14 @@
 
 fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
 
-(*The single theorems go BEFORE the multiple ones. Blacklist is applied to all.*)
+(* The single-name theorems go after the multiple-name ones, so that single
+   names are preferred when both are available. *)
 fun name_thm_pairs respect_no_atp ctxt =
   let
     val (mults, singles) =
       List.partition is_multi (all_valid_thms respect_no_atp ctxt)
-    val ps = [] |> fold add_multi_names mults
-                |> fold add_single_names singles
+    val ps = [] |> fold add_single_names singles
+                |> fold add_multi_names mults
   in ps |> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) end;
 
 fun check_named ("", th) =
diff -r 2a9d0ec8c10d -r ed99188882b1 src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Fri Apr 30 13:47:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Fri Apr 30 14:00:47 2010 +0200
@@ -44,9 +44,11 @@
     TyConstr of name * fol_type list
   val string_of_fol_type :
     fol_type -> name_pool option -> string * name_pool option
-  datatype type_literal = LTVar of string * string | LTFree of string * string
+  datatype type_literal =
+    TyLitVar of string * name |
+    TyLitFree of string * name
   exception CLAUSE of string * term
-  val add_typs : typ list -> type_literal list
+  val add_type_literals : typ list -> type_literal list
   val get_tvar_strs: typ list -> string list
   datatype arLit =
       TConsLit of class * string * string list
@@ -68,7 +70,7 @@
     arity_clause -> int Symtab.table -> int Symtab.table
   val init_functab: int Symtab.table
   val dfg_sign: bool -> string -> string
-  val dfg_of_typeLit: bool -> type_literal -> string
+  val dfg_of_type_literal: bool -> type_literal -> string
   val gen_dfg_cls: int * string * kind * string list * string list * string list -> string
   val string_of_preds: (string * Int.int) list -> string
   val string_of_funcs: (string * int) list -> string
@@ -79,7 +81,8 @@
   val dfg_classrel_clause: classrel_clause -> string
   val dfg_arity_clause: arity_clause -> string
   val tptp_sign: bool -> string -> string
-  val tptp_of_typeLit : bool -> type_literal -> string
+  val tptp_of_type_literal :
+    bool -> type_literal -> name_pool option -> string * name_pool option
   val gen_tptp_cls : int * string * kind * string list * string list -> string
   val tptp_tfree_clause : string -> string
   val tptp_arity_clause : arity_clause -> string
@@ -173,9 +176,7 @@
 fun paren_pack [] = ""   (*empty argument list*)
   | paren_pack strings = "(" ^ commas strings ^ ")";
 
-(*TSTP format uses (...) rather than the old [...]*)
-fun tptp_pack strings = "(" ^ space_implode " | " strings ^ ")";
-
+fun tptp_clause strings = "(" ^ space_implode " | " strings ^ ")"
 
 (*Remove the initial ' character from a type variable, if it is present*)
 fun trim_type_var s =
@@ -230,9 +231,9 @@
 fun empty_name_pool readable_names =
   if readable_names then SOME (`I Symtab.empty) else NONE
 
+fun pool_fold f xs z = pair z #> fold_rev (fn x => uncurry (f x)) xs
 fun pool_map f xs =
-  fold_rev (fn x => fn (ys, pool) => f x pool |>> (fn y => y :: ys)) xs
-  o pair []
+  pool_fold (fn x => fn ys => fn pool => f x pool |>> (fn y => y :: ys)) xs []
 
 fun add_nice_name full_name nice_prefix j the_pool =
   let
@@ -306,8 +307,10 @@
       val (ss, pool) = pool_map string_of_fol_type tys pool
     in (s ^ paren_pack ss, pool) end
 
-(*First string is the type class; the second is a TVar or TFfree*)
-datatype type_literal = LTVar of string * string | LTFree of string * string;
+(* The first component is the type class; the second is a TVar or TFree. *)
+datatype type_literal =
+  TyLitVar of string * name |
+  TyLitFree of string * name
 
 exception CLAUSE of string * term;
 
@@ -317,21 +320,21 @@
       let val sorts = sorts_on_typs_aux ((x,i), ss)
       in
           if s = "HOL.type" then sorts
-          else if i = ~1 then LTFree(make_type_class s, make_fixed_type_var x) :: sorts
-          else LTVar(make_type_class s, make_schematic_type_var (x,i)) :: sorts
+          else if i = ~1 then TyLitFree (make_type_class s, `make_fixed_type_var x) :: sorts
+          else TyLitVar (make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts
       end;
 
 fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s)
   | sorts_on_typs (TVar (v,s))  = sorts_on_typs_aux (v,s);
 
-fun pred_of_sort (LTVar (s,ty)) = (s,1)
-  | pred_of_sort (LTFree (s,ty)) = (s,1)
+fun pred_of_sort (TyLitVar (s, _)) = (s, 1)
+  | pred_of_sort (TyLitFree (s, _)) = (s, 1)
 
 (*Given a list of sorted type variables, return a list of type literals.*)
-fun add_typs Ts = fold (union (op =)) (map sorts_on_typs Ts) []
+fun add_type_literals Ts = fold (union (op =)) (map sorts_on_typs Ts) []
 
 (*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear.
-  * Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a
+  *  Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a
     in a lemma has the same sort as 'a in the conjecture.
   * Deleting such clauses will lead to problems with locales in other use of local results
     where 'a is fixed. Probably we should delete clauses unless the sorts agree.
@@ -499,8 +502,10 @@
 fun dfg_sign true s = s
   | dfg_sign false s = "not(" ^ s ^ ")"
 
-fun dfg_of_typeLit pos (LTVar (s,ty))  = dfg_sign pos (s ^ "(" ^ ty ^ ")")
-  | dfg_of_typeLit pos (LTFree (s,ty)) = dfg_sign pos (s ^ "(" ^ ty ^ ")");
+fun dfg_of_type_literal pos (TyLitVar (s, (s', _))) =
+    dfg_sign pos (s ^ "(" ^ s' ^ ")")
+  | dfg_of_type_literal pos (TyLitFree (s, (s', _))) =
+    dfg_sign pos (s ^ "(" ^ s' ^ ")");
 
 (*Enclose the clause body by quantifiers, if necessary*)
 fun dfg_forall [] body = body
@@ -563,21 +568,23 @@
 fun tptp_sign true s = s
   | tptp_sign false s = "~ " ^ s
 
-fun tptp_of_typeLit pos (LTVar (s, ty))  = tptp_sign pos (s ^ "(" ^ ty ^ ")")
-  | tptp_of_typeLit pos (LTFree (s, ty)) = tptp_sign pos (s ^ "(" ^ ty ^ ")")
+fun tptp_of_type_literal pos (TyLitVar (s, name)) =
+    nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")"))
+  | tptp_of_type_literal pos (TyLitFree (s, name)) =
+    nice_name name #>> (fn s' => tptp_sign pos (s ^ "(" ^ s' ^ ")"))
 
 fun tptp_cnf name kind formula =
   "cnf(" ^ name ^ ", " ^ kind ^ ",\n    " ^ formula ^ ").\n"
 
 fun gen_tptp_cls (cls_id, ax_name, Axiom, lits, tylits) =
       tptp_cnf (string_of_clausename (cls_id, ax_name)) "axiom"
-               (tptp_pack (tylits @ lits))
+               (tptp_clause (tylits @ lits))
   | gen_tptp_cls (cls_id, ax_name, Conjecture, lits, _) =
       tptp_cnf (string_of_clausename (cls_id, ax_name)) "negated_conjecture"
-               (tptp_pack lits)
+               (tptp_clause lits)
 
 fun tptp_tfree_clause tfree_lit =
-    tptp_cnf "tfree_tcs" "negated_conjecture" (tptp_pack [tfree_lit])
+    tptp_cnf "tfree_tcs" "negated_conjecture" (tptp_clause [tfree_lit])
 
 fun tptp_of_arLit (TConsLit (c,t,args)) =
       tptp_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")")
@@ -586,11 +593,11 @@
 
 fun tptp_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) =
   tptp_cnf (string_of_ar axiom_name) "axiom"
-           (tptp_pack (map tptp_of_arLit (conclLit :: premLits)))
+           (tptp_clause (map tptp_of_arLit (conclLit :: premLits)))
 
 fun tptp_classrelLits sub sup =
   let val tvar = "(T)"
-  in  tptp_pack [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)]  end;
+  in  tptp_clause [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)]  end;
 
 fun tptp_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) =
   tptp_cnf axiom_name "axiom" (tptp_classrelLits subclass superclass)
diff -r 2a9d0ec8c10d -r ed99188882b1 src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Fri Apr 30 13:47:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Fri Apr 30 14:00:47 2010 +0200
@@ -302,9 +302,13 @@
  
 (* Given a clause, returns its literals paired with a list of literals
    concerning TFrees; the latter should only occur in conjecture clauses. *)
-fun tptp_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) =
-  pool_map (tptp_literal params) literals
-  #>> rpair (map (tptp_of_typeLit pos) (add_typs ctypes_sorts))
+fun tptp_type_literals params pos (HOLClause {literals, ctypes_sorts, ...})
+                       pool =
+  let
+    val (lits, pool) = pool_map (tptp_literal params) literals pool
+    val (tylits, pool) = pool_map (tptp_of_type_literal pos)
+                                  (add_type_literals ctypes_sorts) pool
+  in ((lits, tylits), pool) end
 
 fun tptp_clause params (cls as HOLClause {axiom_name, clause_id, kind, ...})
                 pool =
@@ -323,7 +327,7 @@
 
 fun dfg_type_literals params pos (HOLClause {literals, ctypes_sorts, ...}) =
   pool_map (dfg_literal params) literals
-  #>> rpair (map (dfg_of_typeLit pos) (add_typs ctypes_sorts))
+  #>> rpair (map (dfg_of_type_literal pos) (add_type_literals ctypes_sorts))
 
 fun get_uvars (CombConst _) vars pool = (vars, pool)
   | get_uvars (CombVar (name, _)) vars pool =
@@ -354,19 +358,19 @@
 fun add_types tvars = fold add_fol_type_funcs tvars
 
 fun add_decls (full_types, explicit_apply, cma, cnh)
-              (CombConst ((c, _), _, tvars)) (funcs, preds) =
-      if c = "equal" then
-        (add_types tvars funcs, preds)
-      else
-        let val arity = min_arity_of cma c
-            val ntys = if not full_types then length tvars else 0
-            val addit = Symtab.update(c, arity+ntys)
-        in
-            if needs_hBOOL explicit_apply cnh c then
-              (add_types tvars (addit funcs), preds)
-            else
-              (add_types tvars funcs, addit preds)
-        end
+              (CombConst ((c, _), ctp, tvars)) (funcs, preds) =
+      (if c = "equal" then
+         (add_types tvars funcs, preds)
+       else
+         let val arity = min_arity_of cma c
+             val ntys = if not full_types then length tvars else 0
+             val addit = Symtab.update(c, arity + ntys)
+         in
+             if needs_hBOOL explicit_apply cnh c then
+               (add_types tvars (addit funcs), preds)
+             else
+               (add_types tvars funcs, addit preds)
+         end) |>> full_types ? add_fol_type_funcs ctp
   | add_decls _ (CombVar (_, ctp)) (funcs, preds) =
       (add_fol_type_funcs ctp funcs, preds)
   | add_decls params (CombApp (P, Q)) decls =
diff -r 2a9d0ec8c10d -r ed99188882b1 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Apr 30 13:47:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Apr 30 14:00:47 2010 +0200
@@ -42,7 +42,16 @@
 fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
 fun is_head_digit s = Char.isDigit (String.sub (s, 0))
 
+(* Hack: Could return false positives (e.g., a user happens to declare a
+   constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
+val is_skolem_const_name =
+  Long_Name.base_name
+  #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
+
+val index_in_shape = find_index o exists o curry (op =)
 fun is_axiom_clause_number thm_names num = num <= Vector.length thm_names
+fun is_conjecture_clause_number conjecture_shape num =
+  index_in_shape num conjecture_shape >= 0
 
 fun ugly_name NONE s = s
   | ugly_name (SOME the_pool) s =
@@ -51,15 +60,13 @@
     | NONE => s
 
 fun smart_lambda v t =
-    Abs (case v of
-           Const (s, _) =>
-           List.last (space_explode skolem_infix (Long_Name.base_name s))
-         | Var ((s, _), _) => s
-         | Free (s, _) => s
-         | _ => "", fastype_of v, abstract_over (v, t))
-
+  Abs (case v of
+         Const (s, _) =>
+         List.last (space_explode skolem_infix (Long_Name.base_name s))
+       | Var ((s, _), _) => s
+       | Free (s, _) => s
+       | _ => "", fastype_of v, abstract_over (v, t))
 fun forall_of v t = HOLogic.all_const (fastype_of v) $ smart_lambda v t
-fun exists_of v t = HOLogic.exists_const (fastype_of v) $ smart_lambda v t
 
 datatype ('a, 'b, 'c, 'd, 'e) raw_step =
   Definition of 'a * 'b * 'c |
@@ -67,13 +74,30 @@
 
 (**** PARSING OF TSTP FORMAT ****)
 
+fun strip_spaces_in_list [] = ""
+  | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1
+  | strip_spaces_in_list [c1, c2] =
+    strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2]
+  | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) =
+    if Char.isSpace c1 then
+      strip_spaces_in_list (c2 :: c3 :: cs)
+    else if Char.isSpace c2 then
+      if Char.isSpace c3 then
+        strip_spaces_in_list (c1 :: c3 :: cs)
+      else
+        str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^
+        strip_spaces_in_list (c3 :: cs)
+    else
+      str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
+val strip_spaces = strip_spaces_in_list o String.explode
+
 (* Syntax trees, either term list or formulae *)
 datatype node = IntLeaf of int | StrNode of string * node list
 
-fun atom x = StrNode (x, [])
+fun str_leaf s = StrNode (s, [])
 
 fun scons (x, y) = StrNode ("cons", [x, y])
-val slist_of = List.foldl scons (atom "nil")
+val slist_of = List.foldl scons (str_leaf "nil")
 
 (*Strings enclosed in single quotes, e.g. filenames*)
 val parse_quoted = $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode;
@@ -81,19 +105,22 @@
 (*Integer constants, typically proof line numbers*)
 val parse_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
 
+val parse_dollar_name =
+  Scan.repeat ($$ "$") -- Symbol.scan_id >> (fn (ss, s) => implode ss ^ s)
+
 (* needed for SPASS's output format *)
-fun repair_bool_literal "true" = "c_True"
-  | repair_bool_literal "false" = "c_False"
-fun repair_name pool "equal" = "c_equal"
+fun repair_name _ "$true" = "c_True"
+  | repair_name _ "$false" = "c_False"
+  | repair_name _ "$$e" = "c_equal" (* seen in Vampire 11 proofs *)
+  | repair_name _ "equal" = "c_equal" (* probably not needed *)
   | repair_name pool s = ugly_name pool s
 (* Generalized first-order terms, which include file names, numbers, etc. *)
 (* The "x" argument is not strictly necessary, but without it Poly/ML loops
    forever at compile time. *)
 fun parse_term pool x =
-     (parse_quoted >> atom
+     (parse_quoted >> str_leaf
    || parse_integer >> IntLeaf
-   || $$ "$" |-- Symbol.scan_id >> (atom o repair_bool_literal)
-   || (Symbol.scan_id >> repair_name pool)
+   || (parse_dollar_name >> repair_name pool)
       -- Scan.optional ($$ "(" |-- parse_terms pool --| $$ ")") [] >> StrNode
    || $$ "(" |-- parse_term pool --| $$ ")"
    || $$ "[" |-- Scan.optional (parse_terms pool) [] --| $$ "]" >> slist_of) x
@@ -112,16 +139,16 @@
   parse_term pool -- Scan.option (Scan.option ($$ "!") --| $$ "="
                                   -- parse_term pool)
   >> repair_predicate_term
-(* Literals can involve "~", "=", and "!=". *)
 fun parse_literal pool x =
   ($$ "~" |-- parse_literal pool >> negate_node || parse_predicate_term pool) x
-
 fun parse_literals pool =
   parse_literal pool ::: Scan.repeat ($$ "|" |-- parse_literal pool)
-
-(* Clause: a list of literals separated by disjunction operators ("|"). *)
+fun parse_parenthesized_literals pool =
+  $$ "(" |-- parse_literals pool --| $$ ")" || parse_literals pool
 fun parse_clause pool =
-  $$ "(" |-- parse_literals pool --| $$ ")" || Scan.single (parse_literal pool)
+  parse_parenthesized_literals pool
+    ::: Scan.repeat ($$ "|" |-- parse_parenthesized_literals pool)
+  >> List.concat
 
 fun ints_of_node (IntLeaf n) = cons n
   | ints_of_node (StrNode (_, us)) = fold ints_of_node us
@@ -161,24 +188,31 @@
 (* It is not clear why some literals are followed by sequences of stars. We
    ignore them. *)
 fun parse_starred_predicate_term pool =
-  parse_predicate_term pool --| Scan.repeat ($$ "*" || $$ " ")
+  parse_predicate_term pool --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")
 
 fun parse_horn_clause pool =
-  Scan.repeat (parse_starred_predicate_term pool) --| $$ "-" --| $$ ">"
-  -- Scan.repeat (parse_starred_predicate_term pool)
-  >> (fn ([], []) => [atom "c_False"]
-       | (clauses1, clauses2) => map negate_node clauses1 @ clauses2)
+  Scan.repeat (parse_starred_predicate_term pool) --| $$ "|" --| $$ "|"
+    -- Scan.repeat (parse_starred_predicate_term pool) --| $$ "-" --| $$ ">"
+    -- Scan.repeat (parse_starred_predicate_term pool)
+  >> (fn (([], []), []) => [str_leaf "c_False"]
+       | ((clauses1, clauses2), clauses3) =>
+         map negate_node (clauses1 @ clauses2) @ clauses3)
 
-(* Syntax: <num>[0:<inference><annotations>] ||
-           <cnf_formulas> -> <cnf_formulas>. *)
+(* Syntax: <num>[0:<inference><annotations>]
+   <cnf_formulas> || <cnf_formulas> -> <cnf_formulas>. *)
 fun finish_spass_line ((num, deps), us) = Inference (num, us, deps)
 fun parse_spass_line pool =
   parse_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
-  -- parse_spass_annotations --| $$ "]" --| $$ "|" --| $$ "|"
-  -- parse_horn_clause pool --| $$ "."
+  -- parse_spass_annotations --| $$ "]" -- parse_horn_clause pool --| $$ "."
   >> finish_spass_line
 
-fun parse_line pool = fst o (parse_tstp_line pool || parse_spass_line pool)
+fun parse_line pool = parse_tstp_line pool || parse_spass_line pool
+fun parse_lines pool = Scan.repeat1 (parse_line pool)
+fun parse_proof pool =
+  fst o Scan.finite Symbol.stopper
+            (Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")
+                            (parse_lines pool)))
+  o explode o strip_spaces
 
 (**** INTERPRETATION OF TSTP SYNTAX TREES ****)
 
@@ -346,28 +380,48 @@
 
 (*Update TVars/TFrees with detected sort constraints.*)
 fun repair_sorts vt =
-  let fun tysubst (Type (a, Ts)) = Type (a, map tysubst Ts)
-        | tysubst (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup vt xi))
-        | tysubst (TFree (x, s)) = TFree (x, the_default s (Vartab.lookup vt (x, ~1)))
-      fun tmsubst (Const (a, T)) = Const (a, tysubst T)
-        | tmsubst (Free (a, T)) = Free (a, tysubst T)
-        | tmsubst (Var (xi, T)) = Var (xi, tysubst T)
-        | tmsubst (t as Bound _) = t
-        | tmsubst (Abs (a, T, t)) = Abs (a, tysubst T, tmsubst t)
-        | tmsubst (t1 $ t2) = tmsubst t1 $ tmsubst t2
-  in not (Vartab.is_empty vt) ? tmsubst end;
+  let
+    fun do_type (Type (a, Ts)) = Type (a, map do_type Ts)
+      | do_type (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup vt xi))
+      | do_type (TFree (x, s)) =
+        TFree (x, the_default s (Vartab.lookup vt (x, ~1)))
+    fun do_term (Const (a, T)) = Const (a, do_type T)
+      | do_term (Free (a, T)) = Free (a, do_type T)
+      | do_term (Var (xi, T)) = Var (xi, do_type T)
+      | do_term (t as Bound _) = t
+      | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t)
+      | do_term (t1 $ t2) = do_term t1 $ do_term t2
+  in not (Vartab.is_empty vt) ? do_term end
+
+fun unskolemize_term t =
+  fold forall_of (Term.add_consts t []
+                 |> filter (is_skolem_const_name o fst) |> map Const) t
+
+val combinator_table =
+  [(@{const_name COMBI}, @{thm COMBI_def_raw}),
+   (@{const_name COMBK}, @{thm COMBK_def_raw}),
+   (@{const_name COMBB}, @{thm COMBB_def_raw}),
+   (@{const_name COMBC}, @{thm COMBC_def_raw}),
+   (@{const_name COMBS}, @{thm COMBS_def_raw})]
+
+fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2))
+  | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t')
+  | uncombine_term (t as Const (x as (s, _))) =
+    (case AList.lookup (op =) combinator_table s of
+       SOME thm => thm |> prop_of |> specialize_type @{theory} x |> Logic.dest_equals |> snd
+     | NONE => t)
+  | uncombine_term t = t
 
 (* Interpret a list of syntax trees as a clause, given by "real" literals and
    sort constraints. "vt" holds the initial sort constraints, from the
    conjecture clauses. *)
 fun clause_of_nodes ctxt vt us =
-  let val (vt, dt) = lits_of_nodes (ProofContext.theory_of ctxt) (vt, []) us in
-    dt |> repair_sorts vt
+  let val (vt, t) = lits_of_nodes (ProofContext.theory_of ctxt) (vt, []) us in
+    t |> repair_sorts vt
   end
-fun check_clause ctxt =
+fun check_formula ctxt =
   TypeInfer.constrain HOLogic.boolT
   #> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt)
-fun checked_clause_of_nodes ctxt = check_clause ctxt oo clause_of_nodes ctxt
 
 (** Global sort constraints on TFrees (from tfree_tcs) are positive unit
     clauses. **)
@@ -394,22 +448,26 @@
 
 fun decode_line vt (Definition (num, u, us)) ctxt =
     let
-      val cl1 = clause_of_nodes ctxt vt [u]
-      val vars = snd (strip_comb cl1)
+      val t1 = clause_of_nodes ctxt vt [u]
+      val vars = snd (strip_comb t1)
       val frees = map unvarify_term vars
       val unvarify_args = subst_atomic (vars ~~ frees)
-      val cl2 = clause_of_nodes ctxt vt us
-      val (cl1, cl2) =
-        HOLogic.eq_const HOLogic.typeT $ cl1 $ cl2
-        |> unvarify_args |> check_clause ctxt |> HOLogic.dest_eq
+      val t2 = clause_of_nodes ctxt vt us
+      val (t1, t2) =
+        HOLogic.eq_const HOLogic.typeT $ t1 $ t2
+        |> unvarify_args |> uncombine_term |> check_formula ctxt
+        |> HOLogic.dest_eq
     in
-      (Definition (num, cl1, cl2),
-       fold Variable.declare_term (maps OldTerm.term_frees [cl1, cl2]) ctxt)
+      (Definition (num, t1, t2),
+       fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
     end
   | decode_line vt (Inference (num, us, deps)) ctxt =
-    let val cl = us |> clause_of_nodes ctxt vt |> check_clause ctxt in
-      (Inference (num, cl, deps),
-       fold Variable.declare_term (OldTerm.term_frees cl) ctxt)
+    let
+      val t = us |> clause_of_nodes ctxt vt
+                 |> unskolemize_term |> uncombine_term |> check_formula ctxt
+    in
+      (Inference (num, t, deps),
+       fold Variable.declare_term (OldTerm.term_frees t) ctxt)
     end
 fun decode_lines ctxt lines =
   let
@@ -431,9 +489,10 @@
 
 (*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ
   only in type information.*)
-fun add_line _ (line as Definition _) lines = line :: lines
-  | add_line thm_names (Inference (num, t, [])) lines =
-    (* No dependencies: axiom or conjecture clause *)
+fun add_line _ _ (line as Definition _) lines = line :: lines
+  | add_line conjecture_shape thm_names (Inference (num, t, [])) lines =
+    (* No dependencies: axiom, conjecture clause, or internal axioms or
+       definitions (Vampire). *)
     if is_axiom_clause_number thm_names num then
       (* Axioms are not proof lines. *)
       if is_only_type_information t then
@@ -443,9 +502,11 @@
         (_, []) => lines (*no repetition of proof line*)
       | (pre, Inference (num', _, _) :: post) =>
         pre @ map (replace_deps_in_line (num', [num])) post
-    else
+    else if is_conjecture_clause_number conjecture_shape num then
       Inference (num, t, []) :: lines
-  | add_line _ (Inference (num, t, deps)) lines =
+    else
+      map (replace_deps_in_line (num, [])) lines
+  | add_line _ _ (Inference (num, t, deps)) lines =
     (* Type information will be deleted later; skip repetition test. *)
     if is_only_type_information t then
       Inference (num, t, deps) :: lines
@@ -466,21 +527,32 @@
 and delete_dep num lines =
   fold_rev add_nontrivial_line (map (replace_deps_in_line (num, [])) lines) []
 
-fun is_bad_free (Free (a, _)) = String.isPrefix skolem_prefix a
-  | is_bad_free _ = false
+(* ATPs sometimes reuse free variable names in the strangest ways. Surprisingly,
+   removing the offending lines often does the trick. *)
+fun is_bad_free frees (Free x) = not (member (op =) frees x)
+  | is_bad_free _ _ = false
 
-fun add_desired_line _ _ (line as Definition _) (j, lines) = (j, line :: lines)
-  | add_desired_line ctxt _ (Inference (num, t, [])) (j, lines) =
-    (j, Inference (num, t, []) :: lines)  (* conjecture clauses must be kept *)
-  | add_desired_line ctxt shrink_factor (Inference (num, t, deps)) (j, lines) =
+(* Vampire is keen on producing these. *)
+fun is_trivial_formula (@{const Not} $ (Const (@{const_name "op ="}, _)
+                                        $ t1 $ t2)) = (t1 aconv t2)
+  | is_trivial_formula t = false
+
+fun add_desired_line _ _ _ _ _ (line as Definition _) (j, lines) =
+    (j, line :: lines)
+  | add_desired_line ctxt shrink_factor conjecture_shape thm_names frees
+                     (Inference (num, t, deps)) (j, lines) =
     (j + 1,
-     if is_only_type_information t orelse
-        not (null (Term.add_tvars t [])) orelse
-        exists_subterm is_bad_free t orelse
-        (length deps < 2 orelse j mod shrink_factor <> 0) then
-       map (replace_deps_in_line (num, deps)) lines  (* delete line *)
+     if is_axiom_clause_number thm_names num orelse
+        is_conjecture_clause_number conjecture_shape num orelse
+        (not (is_only_type_information t) andalso
+         null (Term.add_tvars t []) andalso
+         not (exists_subterm (is_bad_free frees) t) andalso
+         not (is_trivial_formula t) andalso
+         (null lines orelse (* last line must be kept *)
+          (length deps >= 2 andalso j mod shrink_factor = 0))) then
+       Inference (num, t, deps) :: lines  (* keep line *)
      else
-       Inference (num, t, deps) :: lines)
+       map (replace_deps_in_line (num, deps)) lines)  (* drop line *)
 
 (** EXTRACTING LEMMAS **)
 
@@ -493,8 +565,6 @@
   let
     val tokens_of = String.tokens (not o is_ident_char)
     fun extract_num ("cnf" :: num :: "axiom" :: _) = Int.fromString num
-      | extract_num ("cnf" :: num :: "negated_conjecture" :: _) =
-        Int.fromString num
       | extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num
       | extract_num _ = NONE
   in atp_proof |> split_lines |> map_filter (extract_num o tokens_of) end
@@ -506,10 +576,9 @@
 fun apply_command _ 1 = "by "
   | apply_command 1 _ = "apply "
   | apply_command i _ = "prefer " ^ string_of_int i ^ " apply "
-fun metis_command i n [] =
-    apply_command i n ^ "metis"
-  | metis_command i n xs =
-    apply_command i n ^ "(metis " ^ space_implode " " xs ^ ")"
+fun metis_command i n [] = apply_command i n ^ "metis"
+  | metis_command i n ss =
+    apply_command i n ^ "(metis " ^ space_implode " " ss ^ ")"
 fun metis_line i n xs =
   "Try this command: " ^
   Markup.markup Markup.sendback (metis_command i n xs) ^ ".\n" 
@@ -532,9 +601,6 @@
     val n = Logic.count_prems (prop_of goal)
   in (metis_line i n lemmas ^ minimize_line minimize_command lemmas, lemmas) end
 
-val is_valid_line =
-  String.isPrefix "fof(" orf String.isPrefix "cnf(" orf String.isSubstring "||"
-
 (** Isar proof construction and manipulation **)
 
 fun merge_fact_sets (ls1, ss1) (ls2, ss2) =
@@ -551,13 +617,15 @@
   Assume of label * term |
   Have of qualifier list * label * term * byline
 and byline =
-  Facts of facts |
+  ByMetis of facts |
   CaseSplit of step list list * facts
 
 val raw_prefix = "X"
 val assum_prefix = "A"
 val fact_prefix = "F"
 
+fun string_for_label (s, num) = s ^ string_of_int num
+
 fun add_fact_from_dep thm_names num =
   if is_axiom_clause_number thm_names num then
     apsnd (insert (op =) (Vector.sub (thm_names, num - 1)))
@@ -571,35 +639,19 @@
   | step_for_line thm_names j (Inference (num, t, deps)) =
     Have (if j = 1 then [Show] else [], (raw_prefix, num),
           forall_vars t,
-          Facts (fold (add_fact_from_dep thm_names) deps ([], [])))
+          ByMetis (fold (add_fact_from_dep thm_names) deps ([], [])))
 
-fun strip_spaces_in_list [] = ""
-  | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1
-  | strip_spaces_in_list [c1, c2] =
-    strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2]
-  | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) =
-    if Char.isSpace c1 then
-      strip_spaces_in_list (c2 :: c3 :: cs)
-    else if Char.isSpace c2 then
-      if Char.isSpace c3 then
-        strip_spaces_in_list (c1 :: c3 :: cs)
-      else
-        str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^
-        strip_spaces_in_list (c3 :: cs)
-    else
-      str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
-val strip_spaces = strip_spaces_in_list o String.explode
-
-fun proof_from_atp_proof pool ctxt shrink_factor atp_proof thm_names frees =
+fun proof_from_atp_proof pool ctxt shrink_factor atp_proof conjecture_shape
+                         thm_names frees =
   let
     val lines =
-      atp_proof
-      |> split_lines |> map strip_spaces |> filter is_valid_line
-      |> map (parse_line pool o explode)
+      atp_proof ^ "$" (* the $ sign is a dummy token *)
+      |> parse_proof pool
       |> decode_lines ctxt
-      |> rpair [] |-> fold_rev (add_line thm_names)
+      |> rpair [] |-> fold_rev (add_line conjecture_shape thm_names)
       |> rpair [] |-> fold_rev add_nontrivial_line
-      |> rpair (0, []) |-> fold_rev (add_desired_line ctxt shrink_factor)
+      |> rpair (0, []) |-> fold_rev (add_desired_line ctxt shrink_factor
+                                               conjecture_shape thm_names frees)
       |> snd
   in
     (if null frees then [] else [Fix frees]) @
@@ -618,12 +670,13 @@
    "drop_ls" are those that should be dropped in a case split. *)
 type backpatches = (label * facts) list * (label list * label list)
 
-fun using_of_step (Have (_, _, _, by)) =
+fun used_labels_of_step (Have (_, _, _, by)) =
     (case by of
-       Facts (ls, _) => ls
-     | CaseSplit (proofs, (ls, _)) => fold (union (op =) o using_of) proofs ls)
-  | using_of_step _ = []
-and using_of proof = fold (union (op =) o using_of_step) proof []
+       ByMetis (ls, _) => ls
+     | CaseSplit (proofs, (ls, _)) =>
+       fold (union (op =) o used_labels_of) proofs ls)
+  | used_labels_of_step _ = []
+and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof []
 
 fun new_labels_of_step (Fix _) = []
   | new_labels_of_step (Let _) = []
@@ -644,7 +697,7 @@
           if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t')
                       | _ => false) (tl proofs) andalso
              not (exists (member (op =) (maps new_labels_of proofs))
-                         (using_of proof_tail)) then
+                         (used_labels_of proof_tail)) then
             SOME (l, t, map rev proofs, proof_tail)
           else
             NONE
@@ -657,23 +710,21 @@
   | 1 => [Then]
   | _ => [Ultimately]
 
-val index_in_shape = find_index o exists o curry (op =)
-
 fun redirect_proof thy conjecture_shape hyp_ts concl_t proof =
   let
     val concl_ls = map (pair raw_prefix) (List.last conjecture_shape)
-    fun find_hyp (_, j) = nth hyp_ts (index_in_shape j conjecture_shape)
+    fun find_hyp num = nth hyp_ts (index_in_shape num conjecture_shape)
     fun first_pass ([], contra) = ([], contra)
       | first_pass ((step as Fix _) :: proof, contra) =
         first_pass (proof, contra) |>> cons step
       | first_pass ((step as Let _) :: proof, contra) =
         first_pass (proof, contra) |>> cons step
-      | first_pass ((step as Assume (l, t)) :: proof, contra) =
+      | first_pass ((step as Assume (l as (_, num), t)) :: proof, contra) =
         if member (op =) concl_ls l then
           first_pass (proof, contra ||> cons step)
         else
-          first_pass (proof, contra) |>> cons (Assume (l, find_hyp l))
-      | first_pass ((step as Have (qs, l, t, Facts (ls, ss))) :: proof,
+          first_pass (proof, contra) |>> cons (Assume (l, find_hyp num))
+      | first_pass ((step as Have (qs, l, t, ByMetis (ls, ss))) :: proof,
                     contra) =
         if exists (member (op =) (fst contra)) ls then
           first_pass (proof, contra |>> cons l ||> cons step)
@@ -691,10 +742,10 @@
                   clause_for_literals thy (map (negate_term thy o fst) assums)
                 else
                   concl_t,
-                Facts (backpatch_labels patches (map snd assums)))], patches)
+                ByMetis (backpatch_labels patches (map snd assums)))], patches)
       | second_pass end_qs (Assume (l, t) :: proof, assums, patches) =
         second_pass end_qs (proof, (t, l) :: assums, patches)
-      | second_pass end_qs (Have (qs, l, t, Facts (ls, ss)) :: proof, assums,
+      | second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums,
                             patches) =
         if member (op =) (snd (snd patches)) l andalso
            not (AList.defined (op =) (fst patches) l) then
@@ -710,7 +761,7 @@
                            Assume (l, negate_term thy t)
                          else
                            Have (qs, l, negate_term thy t,
-                                 Facts (backpatch_label patches l)))
+                                 ByMetis (backpatch_label patches l)))
              else
                second_pass end_qs (proof, assums,
                                    patches |>> cons (contra_l, (co_ls, ss)))
@@ -760,7 +811,7 @@
       | do_step (Have (qs, l, t, by)) (proof, subst, assums) =
         (Have (qs, l, t,
                case by of
-                 Facts facts => Facts (relabel_facts subst facts)
+                 ByMetis facts => ByMetis (relabel_facts subst facts)
                | CaseSplit (proofs, facts) =>
                  CaseSplit (map do_proof proofs, relabel_facts subst facts)) ::
          proof, subst, assums)
@@ -768,33 +819,18 @@
     and do_proof proof = fold do_step proof ([], [], []) |> #1 |> rev
   in do_proof end
 
-
-(* Hack: Could return false positives (e.g., a user happens to declare a
-   constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
-val is_skolem_const_name =
-  Long_Name.base_name
-  #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
-
-fun unskolemize_term t =
-  fold exists_of (Term.add_consts t []
-                  |> filter (is_skolem_const_name o fst) |> map Const) t
-
-fun unskolemize_step (Have (qs, l, t, by)) =
-    Have (qs, l, unskolemize_term t, by)
-  | unskolemize_step step = step
-
 val then_chain_proof =
   let
     fun aux _ [] = []
       | aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof
       | aux l' (Have (qs, l, t, by) :: proof) =
         (case by of
-           Facts (ls, ss) =>
+           ByMetis (ls, ss) =>
            Have (if member (op =) ls l' then
                    (Then :: qs, l, t,
-                    Facts (filter_out (curry (op =) l') ls, ss))
+                    ByMetis (filter_out (curry (op =) l') ls, ss))
                  else
-                   (qs, l, t, Facts (ls, ss)))
+                   (qs, l, t, ByMetis (ls, ss)))
          | CaseSplit (proofs, facts) =>
            Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) ::
         aux l proof
@@ -803,17 +839,17 @@
 
 fun kill_useless_labels_in_proof proof =
   let
-    val used_ls = using_of proof
+    val used_ls = used_labels_of proof
     fun do_label l = if member (op =) used_ls l then l else no_label
-    fun kill (Assume (l, t)) = Assume (do_label l, t)
-      | kill (Have (qs, l, t, by)) =
+    fun do_step (Assume (l, t)) = Assume (do_label l, t)
+      | do_step (Have (qs, l, t, by)) =
         Have (qs, do_label l, t,
               case by of
                 CaseSplit (proofs, facts) =>
-                CaseSplit (map (map kill) proofs, facts)
+                CaseSplit (map (map do_step) proofs, facts)
               | _ => by)
-      | kill step = step
-  in map kill proof end
+      | do_step step = step
+  in map do_step proof end
 
 fun prefix_for_depth n = replicate_string (n + 1)
 
@@ -837,10 +873,15 @@
               let
                 val l' = (prefix_for_depth depth fact_prefix, next_fact)
               in (l', (l, l') :: subst, next_fact + 1) end
-          val relabel_facts = apfst (map_filter (AList.lookup (op =) subst))
+          val relabel_facts =
+            apfst (map (fn l =>
+                           case AList.lookup (op =) subst l of
+                             SOME l' => l'
+                           | NONE => raise Fail ("unknown label " ^
+                                                 quote (string_for_label l))))
           val by =
             case by of
-              Facts facts => Facts (relabel_facts facts)
+              ByMetis facts => ByMetis (relabel_facts facts)
             | CaseSplit (proofs, facts) =>
               CaseSplit (map (aux subst (depth + 1) (1, 1)) proofs,
                          relabel_facts facts)
@@ -861,8 +902,7 @@
     fun do_free (s, T) =
       maybe_quote s ^ " :: " ^
       maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T)
-    fun do_raw_label (s, j) = s ^ string_of_int j
-    fun do_label l = if l = no_label then "" else do_raw_label l ^ ": "
+    fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
     fun do_have qs =
       (if member (op =) qs Moreover then "moreover " else "") ^
       (if member (op =) qs Ultimately then "ultimately " else "") ^
@@ -871,18 +911,18 @@
        else
          if member (op =) qs Show then "show" else "have")
     val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
-    fun do_using [] = ""
-      | do_using ls = "using " ^ (space_implode " " (map do_raw_label ls)) ^ " "
-    fun do_by_facts [] = "by metis"
-      | do_by_facts ss = "by (metis " ^ space_implode " " ss ^ ")"
-    fun do_facts (ls, ss) = do_using ls ^ do_by_facts ss
+    fun do_facts (ls, ss) =
+      let
+        val ls = ls |> sort_distinct (prod_ord string_ord int_ord)
+        val ss = ss |> sort_distinct string_ord
+      in metis_command 1 1 (map string_for_label ls @ ss) end
     and do_step ind (Fix xs) =
         do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
       | do_step ind (Let (t1, t2)) =
         do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n"
       | do_step ind (Assume (l, t)) =
         do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
-      | do_step ind (Have (qs, l, t, Facts facts)) =
+      | do_step ind (Have (qs, l, t, ByMetis facts)) =
         do_indent ind ^ do_have qs ^ " " ^
         do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n"
       | do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) =
@@ -898,8 +938,9 @@
         suffix ^ "\n"
       end
     and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
-    (* One-step proofs are pointless; better use the Metis one-liner. *)
-    and do_proof [_] = ""
+    (* One-step proofs are pointless; better use the Metis one-liner
+       directly. *)
+    and do_proof [Have (_, _, _, ByMetis _)] = ""
       | do_proof proof =
         (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
         do_indent 0 ^ "proof -\n" ^
@@ -916,11 +957,10 @@
     val (one_line_proof, lemma_names) =
       metis_proof_text (minimize_command, atp_proof, thm_names, goal, i)
     fun isar_proof_for () =
-      case proof_from_atp_proof pool ctxt shrink_factor atp_proof thm_names
-                                frees
+      case proof_from_atp_proof pool ctxt shrink_factor atp_proof
+                                conjecture_shape thm_names frees
            |> redirect_proof thy conjecture_shape hyp_ts concl_t
            |> kill_duplicate_assumptions_in_proof
-           |> map unskolemize_step
            |> then_chain_proof
            |> kill_useless_labels_in_proof
            |> relabel_proof
@@ -935,7 +975,8 @@
         |> the_default "Warning: The Isar proof construction failed.\n"
   in (one_line_proof ^ isar_proof, lemma_names) end
 
-fun proof_text isar_proof isar_params =
-  if isar_proof then isar_proof_text isar_params else metis_proof_text
+fun proof_text isar_proof isar_params other_params =
+  (if isar_proof then isar_proof_text isar_params else metis_proof_text)
+      other_params
 
 end;
diff -r 2a9d0ec8c10d -r ed99188882b1 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Apr 30 13:47:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Apr 30 14:00:47 2010 +0200
@@ -18,6 +18,8 @@
   val nat_subscript : int -> string
   val unyxml : string -> string
   val maybe_quote : string -> string
+  val monomorphic_term : Type.tyenv -> term -> term
+  val specialize_type : theory -> (string * typ) -> term -> term
 end;
  
 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
@@ -103,4 +105,30 @@
            OuterKeyword.is_keyword s) ? quote
   end
 
+fun monomorphic_term subst t =
+  map_types (map_type_tvar (fn v =>
+      case Type.lookup subst v of
+        SOME typ => typ
+      | NONE => raise TERM ("monomorphic_term: uninstanitated schematic type \
+                            \variable", [t]))) t
+
+fun specialize_type thy (s, T) t =
+  let
+    fun subst_for (Const (s', T')) =
+      if s = s' then
+        SOME (Sign.typ_match thy (T', T) Vartab.empty)
+        handle Type.TYPE_MATCH => NONE
+      else
+        NONE
+    | subst_for (t1 $ t2) =
+      (case subst_for t1 of SOME x => SOME x | NONE => subst_for t2)
+    | subst_for (Abs (_, _, t')) = subst_for t'
+    | subst_for _ = NONE
+  in
+    case subst_for t of
+      SOME subst => monomorphic_term subst t
+    | NONE => raise Type.TYPE_MATCH
+  end
+
+
 end;
diff -r 2a9d0ec8c10d -r ed99188882b1 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Fri Apr 30 13:47:39 2010 +0200
+++ b/src/HOL/Tools/refute.ML	Fri Apr 30 14:00:47 2010 +0200
@@ -70,8 +70,6 @@
   val is_IDT_constructor : theory -> string * typ -> bool
   val is_IDT_recursor : theory -> string * typ -> bool
   val is_const_of_class: theory -> string * typ -> bool
-  val monomorphic_term : Type.tyenv -> term -> term
-  val specialize_type : theory -> (string * typ) -> term -> term
   val string_of_typ : typ -> string
   val typ_of_dtyp : Datatype.descr -> (Datatype.dtyp * typ) list -> Datatype.dtyp -> typ
 end;  (* signature REFUTE *)
@@ -449,57 +447,8 @@
       Term.all T $ Abs (x, T, abstract_over (Var ((x, i), T), t'))) vars t
   end;
 
-(* ------------------------------------------------------------------------- *)
-(* monomorphic_term: applies a type substitution 'typeSubs' for all type     *)
-(*                   variables in a term 't'                                 *)
-(* ------------------------------------------------------------------------- *)
-
-  (* Type.tyenv -> Term.term -> Term.term *)
-
-  fun monomorphic_term typeSubs t =
-    map_types (map_type_tvar
-      (fn v =>
-        case Type.lookup typeSubs v of
-          NONE =>
-          (* schematic type variable not instantiated *)
-          raise REFUTE ("monomorphic_term",
-            "no substitution for type variable " ^ fst (fst v) ^
-            " in term " ^ Syntax.string_of_term_global Pure.thy t)
-        | SOME typ =>
-          typ)) t;
-
-(* ------------------------------------------------------------------------- *)
-(* specialize_type: given a constant 's' of type 'T', which is a subterm of  *)
-(*                  't', where 't' has a (possibly) more general type, the   *)
-(*                  schematic type variables in 't' are instantiated to      *)
-(*                  match the type 'T' (may raise Type.TYPE_MATCH)           *)
-(* ------------------------------------------------------------------------- *)
-
-  (* theory -> (string * Term.typ) -> Term.term -> Term.term *)
-
-  fun specialize_type thy (s, T) t =
-  let
-    fun find_typeSubs (Const (s', T')) =
-      if s=s' then
-        SOME (Sign.typ_match thy (T', T) Vartab.empty)
-          handle Type.TYPE_MATCH => NONE
-      else
-        NONE
-      | find_typeSubs (Free _)           = NONE
-      | find_typeSubs (Var _)            = NONE
-      | find_typeSubs (Bound _)          = NONE
-      | find_typeSubs (Abs (_, _, body)) = find_typeSubs body
-      | find_typeSubs (t1 $ t2)          =
-      (case find_typeSubs t1 of SOME x => SOME x
-                              | NONE   => find_typeSubs t2)
-  in
-    case find_typeSubs t of
-      SOME typeSubs =>
-      monomorphic_term typeSubs t
-    | NONE =>
-      (* no match found - perhaps due to sort constraints *)
-      raise Type.TYPE_MATCH
-  end;
+val monomorphic_term = Sledgehammer_Util.monomorphic_term
+val specialize_type = Sledgehammer_Util.specialize_type
 
 (* ------------------------------------------------------------------------- *)
 (* is_const_of_class: returns 'true' iff 'Const (s, T)' is a constant that   *)