removal of some "ref"s from res_axioms.ML; a side-effect is that the ordering
theorems of Nat.thy are hidden by the Ordering.thy versions

--- a/src/HOL/ATP_Linkup.thy	Thu Sep 27 17:28:05 2007 +0200
+++ b/src/HOL/ATP_Linkup.thy	Thu Sep 27 17:55:28 2007 +0200
@@ -7,7 +7,8 @@
 header{* The Isabelle-ATP Linkup *}
 
 theory ATP_Linkup
-imports Divides Record Hilbert_Choice
+imports Divides Record Hilbert_Choice Presburger Relation_Power SAT Recdef Extraction 
+   (*It must be a parent or a child of every other theory, to prevent theory-merge errors.*)
 uses
   "Tools/polyhash.ML"
   "Tools/res_clause.ML"
@@ -110,4 +111,11 @@
 use "Tools/metis_tools.ML"
 setup MetisTools.setup
 
+(*Sledgehammer*)
+setup ResAxioms.setup
+
+setup {*
+  Theory.at_end ResAxioms.clause_cache_endtheory
+*}
+
 end

--- a/src/HOL/Algebra/Exponent.thy	Thu Sep 27 17:28:05 2007 +0200
+++ b/src/HOL/Algebra/Exponent.thy	Thu Sep 27 17:55:28 2007 +0200
@@ -205,15 +205,10 @@
 apply (rule notnotD)
 apply (rule notI)
 apply (drule contrapos_nn [OF _ leI, THEN notnotD], assumption)
-apply (drule_tac m = a in less_imp_le)
+apply (drule less_imp_le [of a])
 apply (drule le_imp_power_dvd)
 apply (drule_tac n = "p ^ r" in dvd_trans, assumption)
-apply (frule_tac m = k in less_imp_le)
-apply (drule_tac c = m in le_extend_mult, assumption)
-apply (drule_tac k = "p ^ a" and m = " (p ^ a) * m" in dvd_diffD1)
-prefer 2 apply assumption
-apply (rule dvd_refl [THEN dvd_mult2])
-apply (drule_tac n = k in dvd_imp_le, auto)
+apply (metis dvd_diffD1 dvd_triv_right le_extend_mult linorder_linear linorder_not_less mult_commute nat_dvd_not_less)
 done
 
 lemma p_fac_forw: "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |]  

--- a/src/HOL/Algebra/poly/LongDiv.thy	Thu Sep 27 17:28:05 2007 +0200
+++ b/src/HOL/Algebra/poly/LongDiv.thy	Thu Sep 27 17:55:28 2007 +0200
@@ -44,7 +44,7 @@
      [| deg p <= deg r; deg q <= deg r;  
         coeff p (deg r) = - (coeff q (deg r)); deg r ~= 0 |] ==>  
      deg (p + q) < deg r"
-  apply (rule_tac j = "deg r - 1" in le_less_trans)
+  apply (rule le_less_trans [of _ "deg r - 1"])
    prefer 2
    apply arith
   apply (rule deg_aboveI)
@@ -248,13 +248,8 @@
      f = q1 * g + r1; (r1 = 0 | deg r1 < deg g);  
      f = q2 * g + r2; (r2 = 0 | deg r2 < deg g) |] ==> r1 = r2"
   apply (subgoal_tac "q1 = q2")
-   apply clarify
-   apply (rule_tac a = "q2 * g + r1 - q2 * g" and b = "q2 * g + r2 - q2 * g" in box_equals)
-     apply simp
-    apply (simp (no_asm))
-   apply (simp (no_asm))
-  apply (rule long_div_quo_unique)
-  apply assumption+
+   apply (metis a_comm a_lcancel m_comm)
+  apply (metis a_comm l_zero long_div_quo_unique m_comm conc)
   done
 
 end

--- a/src/HOL/Complex/ex/NSPrimes.thy	Thu Sep 27 17:28:05 2007 +0200
+++ b/src/HOL/Complex/ex/NSPrimes.thy	Thu Sep 27 17:55:28 2007 +0200
@@ -215,8 +215,7 @@
 apply (rule inj_onI)
 apply (rule ccontr, auto)
 apply (drule injf_max_order_preserving2)
-apply (cut_tac m = x and n = y in less_linear, auto)
-apply (auto dest!: spec)
+apply (metis linorder_antisym_conv3 order_less_le)
 done
 
 lemma infinite_set_has_order_preserving_inj:

--- a/src/HOL/HoareParallel/Gar_Coll.thy	Thu Sep 27 17:28:05 2007 +0200
+++ b/src/HOL/HoareParallel/Gar_Coll.thy	Thu Sep 27 17:55:28 2007 +0200
@@ -185,7 +185,7 @@
   apply (erule_tac x=i in allE , erule (1) notE impE)
   apply simp
   apply clarify
-  apply (drule le_imp_less_or_eq)
+  apply (drule Nat.le_imp_less_or_eq)
   apply (erule disjE)
    apply (subgoal_tac "Suc (ind x)\<le>r")
     apply fast
@@ -276,7 +276,7 @@
    apply (erule_tac x=i in allE , erule (1) notE impE)
    apply simp
    apply clarify
-   apply (drule le_imp_less_or_eq)
+   apply (drule Nat.le_imp_less_or_eq)
    apply (erule disjE)
     apply (subgoal_tac "Suc (ind x)\<le>r")
      apply fast
@@ -309,7 +309,7 @@
  apply (erule_tac x=i in allE , erule (1) notE impE)
  apply simp
  apply clarify
- apply (drule le_imp_less_or_eq)
+ apply (drule Nat.le_imp_less_or_eq)
  apply (erule disjE)
   apply (subgoal_tac "Suc (ind x)\<le>r")
    apply fast

--- a/src/HOL/HoareParallel/Graph.thy	Thu Sep 27 17:28:05 2007 +0200
+++ b/src/HOL/HoareParallel/Graph.thy	Thu Sep 27 17:55:28 2007 +0200
@@ -1,4 +1,3 @@
-
 header {* \chapter{Case Study: Single and Multi-Mutator Garbage Collection Algorithms}
 
 \section {Formalization of the Memory} *}
@@ -337,7 +336,7 @@
  apply(erule_tac P = "\<lambda>i. i < Suc nat \<longrightarrow> ?P i" and x = "nat" in allE)
  apply simp
  apply(case_tac "j\<le>R")
-  apply(drule le_imp_less_or_eq)
+  apply(drule Nat.le_imp_less_or_eq)
   apply(erule disjE)
    apply(erule allE , erule (1) notE impE)
    apply force

--- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Thu Sep 27 17:28:05 2007 +0200
+++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy	Thu Sep 27 17:55:28 2007 +0200
@@ -383,8 +383,7 @@
 apply force
 --{* 1 subgoal left *}
 apply clarify
-apply(drule le_imp_less_or_eq)
-apply(disjE_tac)
+apply(drule Nat.le_imp_less_or_eq)
 apply (simp_all add:Blacks_def)
 done
 

--- a/src/HOL/Hyperreal/Integration.thy	Thu Sep 27 17:28:05 2007 +0200
+++ b/src/HOL/Hyperreal/Integration.thy	Thu Sep 27 17:55:28 2007 +0200
@@ -553,18 +553,15 @@
 done
 
 lemma partition_lt_cancel: "[| partition(a,b) D; D m < D n |] ==> m < n"
-apply (cut_tac m = n and n = "psize D" in less_linear, auto)
-apply (cut_tac m = m and n = n in less_linear)
-apply (cut_tac m = m and n = "psize D" in less_linear)
+apply (cut_tac less_linear [of n "psize D"], auto)
+apply (cut_tac less_linear [of m n])
+apply (cut_tac less_linear [of m "psize D"])
 apply (auto dest: partition_gt)
 apply (drule_tac n = m in partition_lt_gen, auto)
 apply (frule partition_eq_bound)
 apply (drule_tac [2] partition_gt, auto)
-apply (rule ccontr, drule leI, drule le_imp_less_or_eq)
-apply (auto dest: partition_eq_bound)
-apply (rule ccontr, drule leI, drule le_imp_less_or_eq)
-apply (frule partition_eq_bound, assumption)
-apply (drule_tac m = m in partition_eq_bound, auto)
+apply (metis dense_linear_order_class.dlo_simps(8) le_def partition_rhs partition_rhs2)
+apply (metis Nat.le_less_trans dense_linear_order_class.dlo_simps(8) nat_le_linear partition_eq_bound partition_rhs2)
 done
 
 lemma lemma_additivity4_psize_eq:
@@ -577,7 +574,7 @@
 apply (auto intro: partition_lt_Suc)
 apply (drule_tac n = n in partition_lt_gen, assumption)
 apply (arith, arith)
-apply (cut_tac m = na and n = "psize D" in less_linear)
+apply (cut_tac m = na and n = "psize D" in Nat.less_linear)
 apply (auto dest: partition_lt_cancel)
 apply (rule_tac x=N and y=n in linorder_cases)
 apply (drule_tac x = n and P="%m. N \<le> m --> ?f m = ?g m" in spec, simp)
@@ -609,12 +606,8 @@
      "[| partition(a,b) D; D na < D n; D n < D (Suc na);
          n < psize D |]
       ==> False"
-apply (cut_tac m = n and n = "Suc na" in less_linear, auto)
-apply (drule_tac [2] n = n in partition_lt_gen, auto)
-apply (cut_tac m = "psize D" and n = na in less_linear)
-apply (auto simp add: partition_rhs2 less_Suc_eq)
-apply (drule_tac n = na in partition_lt_gen, auto)
-done
+by (metis not_less_eq partition_lt_cancel real_of_nat_less_iff)
+
 
 lemma psize_const [simp]: "psize (%x. k) = 0"
 by (auto simp add: psize_def)

--- a/src/HOL/Hyperreal/Poly.thy	Thu Sep 27 17:28:05 2007 +0200
+++ b/src/HOL/Hyperreal/Poly.thy	Thu Sep 27 17:55:28 2007 +0200
@@ -739,10 +739,7 @@
       ==> EX! n. ([-a, 1] %^ n) divides p &
                  ~(([-a, 1] %^ (Suc n)) divides p)"
 apply (auto intro: poly_order_exists simp add: less_linear simp del: pmult_Cons pexp_Suc)
-apply (cut_tac m = y and n = n in less_linear)
-apply (drule_tac m = n in poly_exp_divides)
-apply (auto dest: Suc_le_eq [THEN iffD2, THEN [2] poly_exp_divides]
-            simp del: pmult_Cons pexp_Suc)
+apply (metis Suc_leI Nat.less_linear poly_exp_divides)
 done
 
 text{*Order*}

--- a/src/HOL/Hyperreal/StarClasses.thy	Thu Sep 27 17:28:05 2007 +0200
+++ b/src/HOL/Hyperreal/StarClasses.thy	Thu Sep 27 17:55:28 2007 +0200
@@ -348,8 +348,8 @@
 
 instance star :: (semiring_0_cancel) semiring_0_cancel ..
 
-instance star :: (comm_semiring) comm_semiring
-by (intro_classes, transfer, rule distrib)
+instance star :: (comm_semiring) comm_semiring 
+by (intro_classes, transfer, rule left_distrib)
 
 instance star :: (comm_semiring_0) comm_semiring_0 ..
 instance star :: (comm_semiring_0_cancel) comm_semiring_0_cancel ..

--- a/src/HOL/IOA/IOA.thy	Thu Sep 27 17:28:05 2007 +0200
+++ b/src/HOL/IOA/IOA.thy	Thu Sep 27 17:55:28 2007 +0200
@@ -251,9 +251,7 @@
    apply (rule_tac x = "Suc n" in exI)
    apply (simp (no_asm))
   apply simp
-  apply (rule allI)
-  apply (cut_tac m = "na" and n = "n" in less_linear)
-  apply auto
+  apply (metis ioa_triple_proj less_antisym)
   done
 
 

--- a/src/HOL/Main.thy	Thu Sep 27 17:28:05 2007 +0200
+++ b/src/HOL/Main.thy	Thu Sep 27 17:55:28 2007 +0200
@@ -11,14 +11,8 @@
 text {*
   Theory @{text Main} includes everything.  Note that theory @{text
   PreList} already includes most HOL theories.
-
-  \medskip Late clause setup: installs \emph{all} known theorems
-  into the clause cache; cf.\ theory @{text ATP_Linkup}. 
-  FIXME: delete once @{text end_theory} actions are installed!
 *}
 
-setup ResAxioms.clause_cache_setup
-
 ML {* val HOL_proofs = !proofs *}
 
 end

--- a/src/HOL/MetisExamples/Abstraction.thy	Thu Sep 27 17:28:05 2007 +0200
+++ b/src/HOL/MetisExamples/Abstraction.thy	Thu Sep 27 17:55:28 2007 +0200
@@ -90,13 +90,20 @@
 apply (metis Collect_mem_eq SigmaD2);
 done
 
-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 llabs_subgoal_1"
-assume 2: "\<And>cl. llabs_subgoal_1 cl = Collect (llabs_Predicate_Xsup_Un_eq_1_ (pset cl))"
-assume 3: "f \<notin> pset cl"
+lemma "(cl,f) \<in> CLF ==> CLF = (SIGMA cl: CL.{f. f \<in> pset cl}) ==> f \<in> pset cl"
+proof (neg_clausify)
+assume 0: "\<And>cl\<Colon>'a\<Colon>type set.
+   (llabs_subgoal_1\<Colon>'a\<Colon>type set \<Rightarrow> 'a\<Colon>type set) cl =
+   Collect (llabs_Set_XCollect_ex_eq_3_ op \<in> (pset cl))"
+assume 1: "(f\<Colon>'a\<Colon>type) \<notin> pset (cl\<Colon>'a\<Colon>type set)"
+assume 2: "(cl\<Colon>'a\<Colon>type set, f\<Colon>'a\<Colon>type) \<in> (CLF\<Colon>('a\<Colon>type set \<times> 'a\<Colon>type) set)"
+have 3: "llabs_Predicate_Xsup_Un_eq2_1_ (CLF\<Colon>('a\<Colon>type set \<times> 'a\<Colon>type) set)
+ (cl\<Colon>'a\<Colon>type set) (f\<Colon>'a\<Colon>type)"
+  by (metis acc_def 2)
+assume 4: "(CLF\<Colon>('a\<Colon>type set \<times> 'a\<Colon>type) set) =
+Sigma (CL\<Colon>'a\<Colon>type set set) (llabs_subgoal_1\<Colon>'a\<Colon>type set \<Rightarrow> 'a\<Colon>type set)"
 show "False"
-  by (metis 0 1 SigmaD2 3 2 Collect_mem_eq)
+  by (metis 1 Collect_mem_eq 0 3 4 acc_def SigmaD2)
 qed finish_clausify (*ugly hack: combinators??*)
 
 ML{*ResAtp.problem_name := "Abstraction__Sigma_Collect_Pi"*}
@@ -110,15 +117,16 @@
     "(cl,f) \<in> (SIGMA cl::'a set : CL. {f. f \<in> pset cl \<rightarrow> pset cl}) ==> 
     f \<in> pset cl \<rightarrow> pset cl"
 proof (neg_clausify)
-assume 0: "(cl, f) \<in> Sigma CL llabs_subgoal_1"
-assume 1: "\<And>cl. llabs_subgoal_1 cl =
-     Collect
-      (llabs_Predicate_Xsup_Un_eq_1_ (Pi (pset cl) (COMBK (pset cl))))"
-assume 2: "f \<notin> Pi (pset cl) (COMBK (pset cl))"
-have 3: "\<not> llabs_Predicate_Xsup_Un_eq_1_ (Pi (pset cl) (COMBK (pset cl))) f"
-  by (metis Collect_mem_eq 2)
+assume 0: "\<And>cl\<Colon>'a\<Colon>type set.
+   (llabs_subgoal_1\<Colon>'a\<Colon>type set \<Rightarrow> ('a\<Colon>type \<Rightarrow> 'a\<Colon>type) set) cl =
+   Collect
+    (llabs_Set_XCollect_ex_eq_3_ op \<in> (Pi (pset cl) (COMBK (pset cl))))"
+assume 1: "(f\<Colon>'a\<Colon>type \<Rightarrow> 'a\<Colon>type) \<notin> Pi (pset (cl\<Colon>'a\<Colon>type set)) (COMBK (pset cl))"
+assume 2: "(cl\<Colon>'a\<Colon>type set, f\<Colon>'a\<Colon>type \<Rightarrow> 'a\<Colon>type)
+\<in> Sigma (CL\<Colon>'a\<Colon>type set set)
+   (llabs_subgoal_1\<Colon>'a\<Colon>type set \<Rightarrow> ('a\<Colon>type \<Rightarrow> 'a\<Colon>type) set)"
 show "False"
-  by (metis acc_def 0 Collect_mem_eq SigmaD2 3 1 Collect_mem_eq)
+  by (metis 1 Collect_mem_eq 0 SigmaD2 2)
 qed finish_clausify
     (*Hack to prevent the "Additional hypotheses" error*)
 

--- a/src/HOL/MetisExamples/set.thy	Thu Sep 27 17:28:05 2007 +0200
+++ b/src/HOL/MetisExamples/set.thy	Thu Sep 27 17:55:28 2007 +0200
@@ -11,7 +11,7 @@
 
 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))"
+               (Q(X,y) | ~Q(y,Z) | S(X,X))" 
 by metis
 (*??But metis can't prove the single-step version...*)
 

--- a/src/HOL/PreList.thy	Thu Sep 27 17:28:05 2007 +0200
+++ b/src/HOL/PreList.thy	Thu Sep 27 17:55:28 2007 +0200
@@ -7,7 +7,7 @@
 header {* A Basis for Building the Theory of Lists *}
 
 theory PreList
-imports Presburger Relation_Power SAT Recdef Extraction Record ATP_Linkup
+imports ATP_Linkup
 uses "Tools/function_package/lexicographic_order.ML"
      "Tools/function_package/fundef_datatype.ML"
 begin
@@ -21,7 +21,4 @@
 setup LexicographicOrder.setup
 setup FundefDatatype.setup
 
-(*Sledgehammer*)
-setup ResAxioms.setup
-
 end

--- a/src/HOL/Tools/meson.ML	Thu Sep 27 17:28:05 2007 +0200
+++ b/src/HOL/Tools/meson.ML	Thu Sep 27 17:55:28 2007 +0200
@@ -209,10 +209,10 @@
 
 (*** The basic CNF transformation ***)
 
-val max_clauses = ref 40;
+val max_clauses = 40;
 
-fun sum x y = if x < !max_clauses andalso y < !max_clauses then x+y else !max_clauses;
-fun prod x y = if x < !max_clauses andalso y < !max_clauses then x*y else !max_clauses;
+fun sum x y = if x < max_clauses andalso y < max_clauses then x+y else max_clauses;
+fun prod x y = if x < max_clauses andalso y < max_clauses then x*y else max_clauses;
 
 (*Estimate the number of clauses in order to detect infeasible theorems*)
 fun signed_nclauses b (Const("Trueprop",_) $ t) = signed_nclauses b t
@@ -239,7 +239,7 @@
 
 val nclauses = signed_nclauses true;
 
-fun too_many_clauses t = nclauses t >= !max_clauses;
+fun too_many_clauses t = nclauses t >= max_clauses;
 
 (*Replaces universally quantified variables by FREE variables -- because
   assumptions may not contain scheme variables.  Later, we call "generalize". *)
@@ -396,7 +396,7 @@
       [] => false (*not a function type, OK*)
     | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts;
 
-(*Raises an exception if any Vars in the theorem mention type bool.
+(*Returns false if any Vars in the theorem mention type bool.
   Also rejects functions whose arguments are Booleans or other functions.*)
 fun is_fol_term thy t =
     Term.is_first_order ["all","All","Ex"] t andalso

--- a/src/HOL/Tools/res_axioms.ML	Thu Sep 27 17:28:05 2007 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Thu Sep 27 17:55:28 2007 +0200
@@ -21,19 +21,13 @@
   val simpset_rules_of: Proof.context -> (string * thm) list  (*FIXME DELETE*)
   val atpset_rules_of: Proof.context -> (string * thm) list
   val meson_method_setup: theory -> theory
-  val clause_cache_setup: theory -> theory
+  val clause_cache_endtheory: theory -> theory option
   val setup: theory -> theory
 end;
 
 structure ResAxioms: RES_AXIOMS =
 struct
 
-(*For running the comparison between combinators and abstractions.
-  CANNOT be a ref, as the setting is used while Isabelle is built.
-  Currently TRUE: the combinator code cannot be used with proof reconstruction
-  because it is not performed by inference!!*)
-val abstract_lambdas = true;
-
 (* FIXME legacy *)
 fun freeze_thm th = #1 (Drule.freeze_thaw th);
 
@@ -74,22 +68,19 @@
            Thm.instantiate ([], [(cterm_of HOL.thy v, ctp_false)]) th
     | _ => th;
 
-(**** Transformation of Clasets and Simpsets into First-Order Axioms ****)
-
-(*Transfer a theorem into theory ATP_Linkup.thy if it is not already
-  inside that theory -- because it's needed for Skolemization *)
-
-(*This will refer to the final version of theory ATP_Linkup.*)
-val recon_thy_ref = Theory.check_thy @{theory}
-
-(*If called while ATP_Linkup is being created, it will transfer to the
-  current version. If called afterward, it will transfer to the final version.*)
-fun transfer_to_ATP_Linkup th =
-    transfer (Theory.deref recon_thy_ref) th handle THM _ => th;
-
+(*To enforce single-threading*)
+exception Clausify_failure of theory;
 
 (**** SKOLEMIZATION BY INFERENCE (lcp) ****)
 
+fun rhs_extra_types lhsT rhs =
+  let val lhs_vars = Term.add_tfreesT lhsT []
+      fun add_new_TFrees (TFree v) =
+	    if member (op =) lhs_vars v then I else insert (op =) (TFree v)
+	| add_new_TFrees _ = I
+      val rhs_consts = fold_aterms (fn Const c => insert (op =) c | _ => I) rhs []
+  in fold (#2 #> Term.fold_atyps add_new_TFrees) rhs_consts [] end;
+
 (*Traverse a theorem, declaring Skolem function definitions. String s is the suggested
   prefix for the Skolem constant. Result is a new theory*)
 fun declare_skofuns s th thy =
@@ -97,18 +88,26 @@
       fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (thy, axs) =
             (*Existential: declare a Skolem function, then insert into body and continue*)
             let val cname = Name.internal ("sko_" ^ s ^ "_" ^ Int.toString (inc nref))
-                val args = term_frees xtp  (*get the formal parameter list*)
-                val Ts = map type_of args
-                val cT = Ts ---> T
+                val args0 = term_frees xtp  (*get the formal parameter list*)
+                val Ts = map type_of args0
+                val extraTs = rhs_extra_types (Ts ---> T) xtp
+                val _ = if null extraTs then () else
+                   warning ("Skolemization: extra type vars: " ^ 
+                            commas_quote (map (Sign.string_of_typ thy) extraTs)); 
+                val argsx = map (fn T => Free(gensym"vsk", T)) extraTs
+                val args = argsx @ args0
+                val cT = extraTs ---> Ts ---> T
                 val c = Const (Sign.full_name thy cname, cT)
                 val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
                         (*Forms a lambda-abstraction over the formal parameters*)
+                val _ = Output.debug (fn () => "declaring the constant " ^ cname)
                 val thy' = Sign.add_consts_authentic [(cname, cT, NoSyn)] thy
                            (*Theory is augmented with the constant, then its def*)
                 val cdef = cname ^ "_def"
                 val thy'' = Theory.add_defs_i false false [(cdef, equals cT $ c $ rhs)] thy'
+                            handle ERROR _ => raise Clausify_failure thy'
             in dec_sko (subst_bound (list_comb(c,args), p))
-                       (thy'', get_axiom thy'' cdef :: axs)
+			       (thy'', get_axiom thy'' cdef :: axs)
             end
         | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) thx =
             (*Universal quant: insert a free variable into body and continue*)
@@ -280,6 +279,7 @@
                           val cdef = cname ^ "_def"
                           val thy = Theory.add_defs_i false false
                                        [(cdef, equals cT $ c $ rhs)] thy
+                                    handle ERROR _ => raise Clausify_failure thy
                           val _ = Output.debug (fn()=> "Definition is " ^ string_of_thm (get_axiom thy cdef));
                           val ax = get_axiom thy cdef |> freeze_thm
                                      |> mk_object_eq |> strip_lambdas (length args)
@@ -402,6 +402,17 @@
        |> Thm.varifyT
   end;
 
+
+(*This will refer to the final version of theory ATP_Linkup.*)
+val atp_linkup_thy_ref = Theory.check_thy @{theory}
+
+(*Transfer a theorem into theory ATP_Linkup.thy if it is not already
+  inside that theory -- because it's needed for Skolemization.
+  If called while ATP_Linkup is being created, it will transfer to the
+  current version. If called afterward, it will transfer to the final version.*)
+fun transfer_to_ATP_Linkup th =
+    transfer (Theory.deref atp_linkup_thy_ref) th handle THM _ => th;
+
 (*Converts an Isabelle theorem (intro, elim or simp format, even higher-order) into NNF.*)
 fun to_nnf th =
     th |> transfer_to_ATP_Linkup
@@ -423,26 +434,21 @@
           |> tap (fn ths => assert_lambda_free ths "assume_abstract: lambdas")
 
 (*Replace lambdas by assumed function definitions in the theorems*)
-fun assume_abstract_list s ths =
-  if abstract_lambdas then List.concat (map (assume_abstract s) ths)
-  else map Drule.eta_contraction_rule ths;
+fun assume_abstract_list s ths = List.concat (map (assume_abstract s) ths);
 
 (*Replace lambdas by declared function definitions in the theorems*)
-fun declare_abstract' s (thy, []) = (thy, [])
-  | declare_abstract' s (thy, th::ths) =
+fun declare_abstract s (thy, []) = (thy, [])
+  | declare_abstract s (thy, th::ths) =
       let val (thy', th_defs) =
             if lambda_free (prop_of th) then (thy, [th])
             else
                 th |> zero_var_indexes |> freeze_thm
                    |> Drule.eta_contraction_rule |> transfer thy |> declare_absfuns s
+                handle Clausify_failure thy_e => (thy_e,[])
           val _ = assert_lambda_free th_defs "declare_abstract: lambdas"
-          val (thy'', ths') = declare_abstract' s (thy', ths)
+          val (thy'', ths') = declare_abstract (s^"'") (thy', ths)
       in  (thy'', th_defs @ ths')  end;
 
-fun declare_abstract s (thy, ths) =
-  if abstract_lambdas then declare_abstract' s (thy, ths)
-  else (thy, map Drule.eta_contraction_rule ths);
-
 (*Keep the full complexity of the original name*)
 fun flatten_name s = space_implode "_X" (NameSpace.explode s);
 
@@ -450,6 +456,10 @@
   if PureThy.has_name_hint th then flatten_name (PureThy.get_name_hint th)
   else gensym "unknown_thm_";
 
+fun name_or_string th =
+  if PureThy.has_name_hint th then PureThy.get_name_hint th
+  else string_of_thm th;
+
 (*Skolemize a named theorem, with Skolem functions as additional premises.*)
 fun skolem_thm th =
   let val nnfth = to_nnf th and s = fake_name th
@@ -461,62 +471,51 @@
   It returns a modified theory, unless skolemization fails.*)
 fun skolem thy th =
      Option.map
-        (fn (nnfth, s) =>
-          let val _ = Output.debug (fn () => "skolemizing " ^ s ^ ": ")
+        (fn nnfth =>
+          let val _ = Output.debug (fn () => "skolemizing " ^ name_or_string th ^ ": ")
+              val _ = Output.debug (fn () => string_of_thm nnfth)
+              val s = fake_name th
               val (thy',defs) = declare_skofuns s nnfth thy
               val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth
+              val _ = Output.debug (fn () => Int.toString (length cnfs) ^ " clauses yielded")
               val (thy'',cnfs') = declare_abstract s (thy',cnfs)
-          in (map Goal.close_result (Meson.finish_cnf cnfs'), thy'')
-          end)
-      (SOME (to_nnf th, fake_name th)  handle THM _ => NONE);
+          in (map Goal.close_result (Meson.finish_cnf cnfs'), thy'') end
+          handle Clausify_failure thy_e => ([],thy_e)
+        )
+      (try to_nnf th);
 
+(*The cache prevents repeated clausification of a theorem, and also repeated declaration of
+  Skolem functions.*)
 structure ThmCache = TheoryDataFun
 (
-  type T = (thm list) Thmtab.table ref;
-  val empty : T = ref Thmtab.empty;
-  fun copy (ref tab) : T = ref tab;
+  type T = (thm list) Thmtab.table;
+  val empty = Thmtab.empty;
+  fun copy tab : T = tab;
   val extend = copy;
-  fun merge _ (ref tab1, ref tab2) : T = ref (Thmtab.merge (K true) (tab1, tab2));
+  fun merge _ (tab1, tab2) : T = Thmtab.merge (K true) (tab1, tab2);
 );
 
-(*The cache prevents repeated clausification of a theorem, and also repeated declaration of
-  Skolem functions. The global one holds theorems proved prior to this point. Theory data
-  holds the remaining ones.*)
-val global_clause_cache = ref (Thmtab.empty : (thm list) Thmtab.table);
-
 (*Populate the clause cache using the supplied theorem. Return the clausal form
   and modified theory.*)
-fun skolem_cache_thm clause_cache th thy =
-  case Thmtab.lookup (!clause_cache) th of
+fun skolem_cache_thm th thy =
+  case Thmtab.lookup (ThmCache.get thy) th of
       NONE =>
         (case skolem thy (Thm.transfer thy th) of
              NONE => ([th],thy)
            | SOME (cls,thy') =>
-                 (if null cls
-                  then warning ("skolem_cache: empty clause set for " ^ string_of_thm th)
-                  else ();
-                  change clause_cache (Thmtab.update (th, cls));
-                  (cls,thy')))
+                 (Output.debug (fn () => "skolem_cache_thm: " ^ Int.toString (length cls) ^ 
+                                         " clauses inserted into cache: " ^ name_or_string th);
+                  (cls, ThmCache.put (Thmtab.update (th,cls) (ThmCache.get thy')) thy')))
     | SOME cls => (cls,thy);
 
 (*Exported function to convert Isabelle theorems into axiom clauses*)
 fun cnf_axiom th =
-  let val cache = ThmCache.get (Thm.theory_of_thm th)
-                  handle ERROR _ => global_clause_cache
-      val in_cache = if cache = global_clause_cache then NONE else Thmtab.lookup (!cache) th
+  let val thy = Theory.merge (Theory.deref atp_linkup_thy_ref, Thm.theory_of_thm th)
   in
-     case in_cache of
-       NONE =>
-         (case Thmtab.lookup (!global_clause_cache) th of
-           NONE =>
-             let val cls = map Goal.close_result (skolem_thm th)
-             in Output.debug (fn () => Int.toString (length cls) ^ " clauses inserted into cache: " ^
-                                 (if PureThy.has_name_hint th then PureThy.get_name_hint th
-                                  else string_of_thm th));
-                change cache (Thmtab.update (th, cls)); cls
-             end
-         | SOME cls => cls)
-     | SOME cls => cls
+      case Thmtab.lookup (ThmCache.get thy) th of
+	  NONE => (Output.debug (fn () => "cnf_axiom: " ^ name_or_string th);
+		   map Goal.close_result (skolem_thm th))
+	| SOME cls => cls
   end;
 
 fun pairname th = (PureThy.get_name_hint th, th);
@@ -572,14 +571,23 @@
 
 (*Setup function: takes a theory and installs ALL known theorems into the clause cache*)
 
-fun skolem_cache clause_cache th thy = #2 (skolem_cache_thm clause_cache th thy);
+val mark_skolemized = Sign.add_consts_i [("ResAxioms_endtheory", HOLogic.boolT, NoSyn)];
+
+fun skolem_cache th thy = #2 (skolem_cache_thm th thy);
+
+fun skolem_cache_all thy = fold skolem_cache (map #2 (PureThy.all_thms_of thy)) thy;
+
+fun skolem_cache_new thy = fold skolem_cache (map #2 (PureThy.thms_of thy)) thy;
 
 (*The cache can be kept smaller by inspecting the prop of each thm. Can ignore all that are
   lambda_free, but then the individual theory caches become much bigger.*)
 
-fun clause_cache_setup thy =
-  fold (skolem_cache global_clause_cache) (map #2 (PureThy.all_thms_of thy)) thy;
-
+(*The new constant is a hack to prevent multiple execution*)
+fun clause_cache_endtheory thy =
+  let val _ = Output.debug (fn () => "RexAxioms end theory action: " ^ Context.str_of_thy thy)
+  in
+    Option.map skolem_cache_new (try mark_skolemized thy)
+  end;
 
 (*** meson proof methods ***)
 
@@ -672,7 +680,7 @@
   | conj_rule ths = foldr1 conj2_rule ths;
 
 fun skolem_attr (Context.Theory thy, th) =
-      let val (cls, thy') = skolem_cache_thm (ThmCache.get thy) th thy
+      let val (cls, thy') = skolem_cache_thm th thy
       in (Context.Theory thy', conj_rule cls) end
   | skolem_attr (context, th) = (context, th)
 
@@ -684,6 +692,6 @@
   [("neg_clausify", Method.no_args (Method.SIMPLE_METHOD' neg_clausify_tac),
     "conversion of goal to conjecture clauses")];
 
-val setup = clause_cache_setup #> ThmCache.init #> setup_attrs #> setup_methods;
+val setup = mark_skolemized #> skolem_cache_all #> ThmCache.init #> setup_attrs #> setup_methods;
 
 end;

--- a/src/HOL/W0/W0.thy	Thu Sep 27 17:28:05 2007 +0200
+++ b/src/HOL/W0/W0.thy	Thu Sep 27 17:55:28 2007 +0200
@@ -208,11 +208,8 @@
      addsimps [thm "free_tv_subst", thm "cod_def", thm "dom_def"])) 1 *})
   -- {* @{text \<Longleftarrow>} *}
   apply (unfold free_tv_subst cod_def dom_def)
-  apply (tactic "safe_tac set_cs")
-   apply (cut_tac m = m and n = n in less_linear)
-   apply (tactic "fast_tac (HOL_cs addSIs [@{thm less_or_eq_imp_le}]) 1")
-  apply (cut_tac m = ma and n = n in less_linear)
-  apply (fast intro!: less_or_eq_imp_le)
+  apply safe
+  apply (metis linorder_not_less)+
   done
 
 lemma new_tv_list: "new_tv n x = (\<forall>y \<in> set x. new_tv n y)"

--- a/src/HOL/ex/Primrec.thy	Thu Sep 27 17:28:05 2007 +0200
+++ b/src/HOL/ex/Primrec.thy	Thu Sep 27 17:55:28 2007 +0200
@@ -219,7 +219,7 @@
 text {* PROPERTY A 11 *}
 
 lemma ack_add_bound: "ack (i1, j) + ack (i2, j) < ack (4 + (i1 + i2), j)"
-  apply (rule_tac j = "ack (Suc (Suc 0), ack (i1 + i2, j))" in less_trans)
+  apply (rule less_trans [of _ "ack (Suc (Suc 0), ack (i1 + i2, j))" _])
    prefer 2
    apply (rule ack_nest_bound [THEN less_le_trans])
    apply (simp add: Suc3_eq_add_3)
@@ -235,11 +235,10 @@
   "\<exists>k'. \<forall>i j. ..."} *}
 
 lemma ack_add_bound2: "i < ack (k, j) ==> i + j < ack (4 + k, j)"
-  apply (rule_tac j = "ack (k, j) + ack (0, j)" in less_trans)
-   prefer 2
+  apply (rule less_trans [of _ "ack (k, j) + ack (0, j)" _])
+   apply (blast intro: add_less_mono less_ack2) 
    apply (rule ack_add_bound [THEN less_le_trans])
    apply simp
-  apply (rule add_less_mono less_ack2 | assumption)+
   done
 
 
@@ -333,7 +332,7 @@
 lemma ack_not_PRIMREC: "\<not> PRIMREC (\<lambda>l. case l of [] => 0 | x # l' => ack (x, x))"
   apply (rule notI)
   apply (erule ack_bounds_PRIMREC [THEN exE])
-  apply (rule less_irrefl)
+  apply (rule Nat.less_irrefl)
   apply (drule_tac x = "[x]" in spec)
   apply simp
   done