diff -r 6ac273f176cd -r 81290fe85890 src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML	Mon Dec 16 12:26:18 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML	Mon Dec 16 14:49:18 2013 +0100
@@ -21,8 +21,8 @@
 open Sledgehammer_Proof
 open Sledgehammer_Preplay
 
-fun variants_of_step (Prove (qs, xs, l, t, subproofs, (facts, _ :: meths))) =
-    map (fn meth => Prove (qs, xs, l, t, subproofs, (facts, [meth]))) meths
+fun variants_of_step (Prove (qs, xs, l, t, subproofs, (facts, methss))) =
+    map (fn meth => Prove (qs, xs, l, t, subproofs, (facts, [[meth]]))) (tl (flat methss))
   | variants_of_step _ = raise Fail "Sledgehammer_Try0: variants_of_step"
 
 val slack = seconds 0.05