# HG changeset patch
# User blanchet
# Date 1387183706 -3600
# Node ID 1c9ef5c834e8e933037079c68e6b732af475325f
# Parent  430ca13d3e54b462f71c680986b3e8fc0185938c
added 'meson' to the mix

diff -r 430ca13d3e54 -r 1c9ef5c834e8 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Mon Dec 16 09:40:02 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Mon Dec 16 09:48:26 2013 +0100
@@ -105,16 +105,17 @@
 fun tac_of_method method type_enc lam_trans ctxt facts =
   (case method of
     MetisM => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts
+  | MesonM => Meson.meson_tac ctxt facts
   | _ =>
     Method.insert_tac facts THEN'
     (case method of
-      SimpM => Simplifier.asm_full_simp_tac
-    | AutoM => Clasimp.auto_tac #> K
-    | FastforceM => Clasimp.fast_force_tac
-    | ForceM => Clasimp.force_tac
-    | ArithM => Arith_Data.arith_tac
-    | BlastM => blast_tac
-    | _ => raise Fail "Sledgehammer_Preplay: tac_of_method") ctxt)
+      SimpM => Simplifier.asm_full_simp_tac ctxt
+    | AutoM => K (Clasimp.auto_tac ctxt)
+    | FastforceM => Clasimp.fast_force_tac ctxt
+    | ForceM => Clasimp.force_tac ctxt
+    | ArithM => Arith_Data.arith_tac ctxt
+    | BlastM => blast_tac ctxt
+    | _ => raise Fail "Sledgehammer_Preplay: tac_of_method"))
 
 (* main function for preplaying Isar steps; may throw exceptions *)
 fun preplay_raw _ _ _ _ _ (Let _) = zero_preplay_time
diff -r 430ca13d3e54 -r 1c9ef5c834e8 src/HOL/Tools/Sledgehammer/sledgehammer_print.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Mon Dec 16 09:40:02 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Mon Dec 16 09:48:26 2013 +0100
@@ -180,6 +180,7 @@
       | ForceM => "force"
       | ArithM => "arith"
       | BlastM => "blast"
+      | MesonM => "meson"
       | _ => raise Fail "Sledgehammer_Print: by_method")
 
     fun using_facts [] [] = ""
diff -r 430ca13d3e54 -r 1c9ef5c834e8 src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Mon Dec 16 09:40:02 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Mon Dec 16 09:48:26 2013 +0100
@@ -26,7 +26,8 @@
     FastforceM |
     ForceM |
     ArithM |
-    BlastM
+    BlastM |
+    MesonM
 
   val no_label : label
   val no_facts : facts
@@ -83,7 +84,8 @@
   FastforceM |
   ForceM |
   ArithM |
-  BlastM
+  BlastM |
+  MesonM
 
 val no_label = ("", ~1)
 val no_facts = ([],[])
diff -r 430ca13d3e54 -r 1c9ef5c834e8 src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML	Mon Dec 16 09:40:02 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML	Mon Dec 16 09:48:26 2013 +0100
@@ -21,7 +21,7 @@
 open Sledgehammer_Proof
 open Sledgehammer_Preplay
 
-val variant_methods = [SimpM, AutoM, ArithM, FastforceM, BlastM, ForceM, MetisM]
+val variant_methods = [SimpM, AutoM, ArithM, FastforceM, BlastM, ForceM, MetisM, MesonM]
 
 fun variants_of_step (Let _) = raise Fail "Sledgehammer_Try0: variants_of_step"
   | variants_of_step (Prove (qs, xs, l, t, subproofs, (facts, meth))) =