diff -r 71fdbffe3275 -r b426cbdb5a23 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Tue Jun 22 13:17:59 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Tue Jun 22 14:28:22 2010 +0200
@@ -47,8 +47,8 @@
 fun string_for_outcome NONE = "Success."
   | string_for_outcome (SOME failure) = string_for_failure failure
 
-fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover
-        timeout subgoal state filtered_clauses name_thms_pairs =
+fun sledgehammer_test_theorems (params : params) prover timeout subgoal state
+                               filtered_clauses name_thms_pairs =
   let
     val num_theorems = length name_thms_pairs
     val _ = priority ("Testing " ^ string_of_int num_theorems ^
@@ -88,7 +88,7 @@
         (result as {outcome = NONE, ...}) => SOME result
       | _ => NONE
 
-    val {context = ctxt, facts, goal} = Proof.goal state;
+    val {context = ctxt, goal, ...} = Proof.goal state;
   in
     (* try prove first to check result and get used theorems *)
     (case test_thms_fun NONE name_thms_pairs of