# HG changeset patch
# User wenzelm
# Date 1243954615 -7200
# Node ID 8c8d615f04aef84018548ebd0f138272a5f4e46e
# Parent  763f4b0fd579eb7c661f208c4dfb00cea764fe3b# Parent  bafd58649c3eae4cc9b59f5accaeddb3fc56969b
merged

diff -r bafd58649c3e -r 8c8d615f04ae src/HOL/Tools/atp_manager.ML
--- a/src/HOL/Tools/atp_manager.ML	Tue Jun 02 16:10:51 2009 +0200
+++ b/src/HOL/Tools/atp_manager.ML	Tue Jun 02 16:56:55 2009 +0200
@@ -81,9 +81,9 @@
   fun ord ((a, _), (b, _)) = Time.compare (a, b);
 );
 
-val lookup_thread = AList.lookup Thread.equal;
-val delete_thread = AList.delete Thread.equal;
-val update_thread = AList.update Thread.equal;
+fun lookup_thread xs = AList.lookup Thread.equal xs;
+fun delete_thread xs = AList.delete Thread.equal xs;
+fun update_thread xs = AList.update Thread.equal xs;
 
 
 (* state of thread manager *)
@@ -104,6 +104,7 @@
 val state = Synchronized.var "atp_manager"
   (make_state NONE ThreadHeap.empty ThreadHeap.empty [] [] [] []);
 
+
 (* unregister thread *)
 
 fun unregister (success, message) thread = Synchronized.change state
diff -r bafd58649c3e -r 8c8d615f04ae src/HOL/Tools/atp_wrapper.ML
--- a/src/HOL/Tools/atp_wrapper.ML	Tue Jun 02 16:10:51 2009 +0200
+++ b/src/HOL/Tools/atp_wrapper.ML	Tue Jun 02 16:56:55 2009 +0200
@@ -113,13 +113,13 @@
 fun tptp_prover_opts max_new theory_const =
   tptp_prover_opts_full max_new theory_const false;
 
-val tptp_prover = tptp_prover_opts 60 true;
+fun tptp_prover x = tptp_prover_opts 60 true x;
 
 (*for structured proofs: prover must support TSTP*)
 fun full_prover_opts max_new theory_const =
   tptp_prover_opts_full max_new theory_const true;
 
-val full_prover = full_prover_opts 60 true;
+fun full_prover x = full_prover_opts 60 true x;
 
 
 (* Vampire *)
diff -r bafd58649c3e -r 8c8d615f04ae src/HOL/Tools/nat_numeral_simprocs.ML
--- a/src/HOL/Tools/nat_numeral_simprocs.ML	Tue Jun 02 16:10:51 2009 +0200
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Tue Jun 02 16:56:55 2009 +0200
@@ -149,7 +149,7 @@
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff
   val find_first_coeff  = find_first_coeff []
-  val trans_tac         = K Arith_Data.trans_tac
+  fun trans_tac _       = Arith_Data.trans_tac
 
   val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @
     [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
@@ -238,7 +238,7 @@
   val dest_coeff        = dest_coeff
   val left_distrib      = @{thm left_add_mult_distrib} RS trans
   val prove_conv        = Arith_Data.prove_conv_nohyps
-  val trans_tac         = K Arith_Data.trans_tac
+  fun trans_tac _       = Arith_Data.trans_tac
 
   val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac}
   val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
@@ -263,7 +263,7 @@
   struct
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff
-  val trans_tac         = K Arith_Data.trans_tac
+  fun trans_tac _       = Arith_Data.trans_tac
 
   val norm_ss1 = Numeral_Simprocs.num_ss addsimps
     numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
@@ -369,7 +369,7 @@
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff
   val find_first        = find_first_t []
-  val trans_tac         = K Arith_Data.trans_tac
+  fun trans_tac _       = Arith_Data.trans_tac
   val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
   fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   val simplify_meta_eq  = cancel_simplify_meta_eq
@@ -380,7 +380,7 @@
   val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_eq
   val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
-  val simp_conv = K(K (SOME @{thm nat_mult_eq_cancel_disj}))
+  fun simp_conv _ _ = SOME @{thm nat_mult_eq_cancel_disj}
 );
 
 structure LessCancelFactor = ExtractCommonTermFun
@@ -388,7 +388,7 @@
   val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
-  val simp_conv = K(K (SOME @{thm nat_mult_less_cancel_disj}))
+  fun simp_conv _ _ = SOME @{thm nat_mult_less_cancel_disj}
 );
 
 structure LeCancelFactor = ExtractCommonTermFun
@@ -396,7 +396,7 @@
   val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
-  val simp_conv = K(K (SOME @{thm nat_mult_le_cancel_disj}))
+  fun simp_conv _ _ = SOME @{thm nat_mult_le_cancel_disj}
 );
 
 structure DivideCancelFactor = ExtractCommonTermFun
@@ -404,7 +404,7 @@
   val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
-  val simp_conv = K(K (SOME @{thm nat_mult_div_cancel_disj}))
+  fun simp_conv _ _ = SOME @{thm nat_mult_div_cancel_disj}
 );
 
 structure DvdCancelFactor = ExtractCommonTermFun
@@ -412,7 +412,7 @@
   val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
   val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT
-  val simp_conv = K(K (SOME @{thm nat_mult_dvd_cancel_disj}))
+  fun simp_conv _ _ = SOME @{thm nat_mult_dvd_cancel_disj}
 );
 
 val cancel_factor =
diff -r bafd58649c3e -r 8c8d615f04ae src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Tue Jun 02 16:10:51 2009 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML	Tue Jun 02 16:56:55 2009 +0200
@@ -232,7 +232,7 @@
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff 1
   val find_first_coeff  = find_first_coeff []
-  val trans_tac         = K Arith_Data.trans_tac
+  fun trans_tac _       = Arith_Data.trans_tac
 
   fun norm_tac ss =
     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
@@ -310,7 +310,7 @@
   val dest_coeff        = dest_coeff 1
   val left_distrib      = @{thm combine_common_factor} RS trans
   val prove_conv        = Arith_Data.prove_conv_nohyps
-  val trans_tac         = K Arith_Data.trans_tac
+  fun trans_tac _       = Arith_Data.trans_tac
 
   fun norm_tac ss =
     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
@@ -336,7 +336,7 @@
   val dest_coeff        = dest_fcoeff 1
   val left_distrib      = @{thm combine_common_factor} RS trans
   val prove_conv        = Arith_Data.prove_conv_nohyps
-  val trans_tac         = K Arith_Data.trans_tac
+  fun trans_tac _       = Arith_Data.trans_tac
 
   val norm_ss1a = norm_ss1 addsimps inverse_1s @ divide_simps
   fun norm_tac ss =
@@ -387,7 +387,7 @@
   struct
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff 1
-  val trans_tac         = K Arith_Data.trans_tac
+  fun trans_tac _       = Arith_Data.trans_tac
 
   val norm_ss1 = HOL_ss addsimps minus_from_mult_simps @ mult_1s
   val norm_ss2 = HOL_ss addsimps simps @ mult_minus_simps
@@ -533,7 +533,7 @@
   val mk_coeff          = mk_coeff
   val dest_coeff        = dest_coeff
   val find_first        = find_first_t []
-  val trans_tac         = K Arith_Data.trans_tac
+  fun trans_tac _       = Arith_Data.trans_tac
   val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
   fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   val simplify_meta_eq  = cancel_simplify_meta_eq 
@@ -545,7 +545,7 @@
   val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_eq
   val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
-  val simp_conv = K (K (SOME @{thm mult_cancel_left}))
+  fun simp_conv _ _ = SOME @{thm mult_cancel_left}
 );
 
 (*for ordered rings*)
@@ -574,7 +574,7 @@
   val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT
-  val simp_conv = K (K (SOME @{thm div_mult_mult1_if}))
+  fun simp_conv _ _ = SOME @{thm div_mult_mult1_if}
 );
 
 structure ModCancelFactor = ExtractCommonTermFun
@@ -582,7 +582,7 @@
   val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binop @{const_name Divides.mod}
   val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} Term.dummyT
-  val simp_conv = K (K (SOME @{thm mod_mult_mult1}))
+  fun simp_conv _ _ = SOME @{thm mod_mult_mult1}
 );
 
 (*for idoms*)
@@ -591,7 +591,7 @@
   val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
   val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} Term.dummyT
-  val simp_conv = K (K (SOME @{thm dvd_mult_cancel_left}))
+  fun simp_conv _ _ = SOME @{thm dvd_mult_cancel_left}
 );
 
 (*Version for all fields, including unordered ones (type complex).*)
@@ -600,7 +600,7 @@
   val prove_conv = Arith_Data.prove_conv
   val mk_bal   = HOLogic.mk_binop @{const_name HOL.divide}
   val dest_bal = HOLogic.dest_bin @{const_name HOL.divide} Term.dummyT
-  val simp_conv = K (K (SOME @{thm mult_divide_mult_cancel_left_if}))
+  fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if}
 );
 
 val cancel_factors =