diff -r e2d58749194b -r 7635bf8918a1 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Aug 25 09:05:22 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Aug 25 09:32:43 2010 +0200
@@ -22,7 +22,6 @@
      relevance_decay: real,
      max_relevant_per_iter: int option,
      theory_relevant: bool option,
-     defs_relevant: bool,
      isar_proof: bool,
      isar_shrink_factor: int,
      timeout: Time.time}
@@ -91,7 +90,6 @@
    relevance_decay: real,
    max_relevant_per_iter: int option,
    theory_relevant: bool option,
-   defs_relevant: bool,
    isar_proof: bool,
    isar_shrink_factor: int,
    timeout: Time.time}
@@ -216,8 +214,8 @@
          explicit_forall, use_conjecture_for_hypotheses}
         ({debug, verbose, overlord, full_types, explicit_apply,
           relevance_threshold, relevance_decay,
-          max_relevant_per_iter, theory_relevant,
-          defs_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
+          max_relevant_per_iter, theory_relevant, isar_proof,
+          isar_shrink_factor, timeout, ...} : params)
         minimize_command
         ({subgoal, goal, relevance_override, axioms} : problem) =
   let
@@ -234,7 +232,6 @@
         SOME axioms => axioms
       | NONE =>
         (relevant_facts full_types relevance_threshold relevance_decay
-                        defs_relevant
                         (the_default default_max_relevant_per_iter
                                      max_relevant_per_iter)
                         (the_default default_theory_relevant theory_relevant)