--- 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