--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Tue Sep 14 23:37:34 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Tue Sep 14 23:38:20 2010 +0200
@@ -52,12 +52,10 @@
(*Traverse a theorem, accumulating Skolem function definitions.*)
fun assume_skolem_funs th =
let
- fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (s', T, p))) rhss =
+ fun dec_sko (Const (@{const_name Ex}, _) $ (body as Abs (_, T, p))) rhss =
(*Existential: declare a Skolem function, then insert into body and continue*)
let
val args = OldTerm.term_frees body
- val Ts = map type_of args
- val cT = Ts ---> T
(* Forms a lambda-abstraction over the formal parameters *)
val rhs =
list_abs_free (map dest_Free args,
@@ -85,7 +83,7 @@
fun extensionalize_theorem th =
case prop_of th of
_ $ (Const (@{const_name HOL.eq}, Type (_, [Type (@{type_name fun}, _), _]))
- $ _ $ Abs (s, _, _)) => extensionalize_theorem (th RS fun_cong_all)
+ $ _ $ Abs _) => extensionalize_theorem (th RS fun_cong_all)
| _ => th
fun is_quasi_lambda_free (Const (@{const_name skolem}, _) $ _) = true
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Sep 14 23:37:34 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Tue Sep 14 23:38:20 2010 +0200
@@ -362,10 +362,12 @@
(* ------------------------------------------------------------------------- *)
(*for debugging only*)
+(*
fun print_thpair (fth,th) =
(trace_msg (fn () => "=============================================");
trace_msg (fn () => "Metis: " ^ Metis.Thm.toString fth);
trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
+*)
fun lookth thpairs (fth : Metis.Thm.thm) =
the (AList.lookup (uncurry Metis.Thm.equal) thpairs fth)
@@ -828,7 +830,6 @@
fun generic_metis_tac mode ctxt ths i st0 =
let
- val thy = ProofContext.theory_of ctxt
val _ = trace_msg (fn () =>
"Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
in
--- a/src/HOL/Tools/async_manager.ML Tue Sep 14 23:37:34 2010 +0200
+++ b/src/HOL/Tools/async_manager.ML Tue Sep 14 23:38:20 2010 +0200
@@ -64,7 +64,7 @@
Synchronized.change global_state
(fn state as {manager, timeout_heap, active, canceling, messages, store} =>
(case lookup_thread active thread of
- SOME (tool, birth_time, _, desc) =>
+ SOME (tool, _, _, desc) =>
let
val active' = delete_thread thread active;
val now = Time.now ()