# HG changeset patch
# User blanchet
# Date 1399232104 -7200
# Node ID d940ad3959c513a6d6f04ab2597acb148f1bd7e1
# Parent  e7a55d295b8e45cf3b36e22271d7d906aad64e3f
use right meson tactic for preplaying

diff -r e7a55d295b8e -r d940ad3959c5 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Sun May 04 21:02:21 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Sun May 04 21:35:04 2014 +0200
@@ -103,7 +103,7 @@
       Metis_Method (type_enc_opt, lam_trans_opt) =>
       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
-    | Meson_Method => Meson.meson_tac ctxt global_facts
+    | Meson_Method => Meson_Tactic.meson_general_tac ctxt global_facts
     | SMT2_Method => SMT2_Solver.smt2_tac ctxt global_facts
     | _ =>
       Method.insert_tac global_facts THEN'