diff -r abab10d1f4a3 -r 547d1a1dcaf6 src/HOL/ex/sledgehammer_tactics.ML
--- a/src/HOL/ex/sledgehammer_tactics.ML	Mon Jan 30 17:15:59 2012 +0100
+++ b/src/HOL/ex/sledgehammer_tactics.ML	Mon Jan 30 17:15:59 2012 +0100
@@ -71,7 +71,7 @@
 fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th =
   case run_atp override_params relevance_override i i ctxt th of
     SOME facts =>
-    Metis_Tactic.metis_tac [] ATP_Problem_Generate.combinatorsN ctxt
+    Metis_Tactic.metis_tac [] ATP_Problem_Generate.combsN ctxt
         (maps (thms_of_name ctxt) facts) i th
   | NONE => Seq.empty