src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML

   | string_for_failure MalformedOutput = "Error."
   | string_for_failure UnknownError = "Failed."
 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 ^
                       " theorem" ^ plural_s num_theorems ^ "...")
     val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs

     fun test_thms filtered thms =
       case test_thms_fun filtered thms of
         (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
       result as {outcome = NONE, pool, internal_thm_names, conjecture_shape,
                  filtered_clauses, ...} =>