diff -r e0233567a8ef -r 54b0352fb46d src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue Feb 04 01:03:28 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue Feb 04 01:35:48 2014 +0100
@@ -94,7 +94,7 @@
   Method.insert_tac local_facts THEN'
   (case meth of
     Metis_Method (type_enc_opt, lam_trans_opt) =>
-    Metis_Tactic.metis_tac [type_enc_opt |> the_default partial_typesN]
+    Metis_Tactic.metis_tac [type_enc_opt |> the_default (hd partial_type_encs)]
       (lam_trans_opt |> the_default default_metis_lam_trans) ctxt global_facts
   | SMT_Method => SMT_Solver.smt_tac ctxt global_facts
   | Meson_Method => Meson.meson_tac ctxt global_facts