# HG changeset patch
# User wenzelm
# Date 1373656494 -7200
# Node ID 564a108d722f4d3cbac17c16dcdecb612973dd41
# Parent  d6f2a7c196f7c263a9a899fae16c14595fbc855c# Parent  fe411c1dc18007d586932dd06d698cafaafa2997
merged

diff -r fe411c1dc180 -r 564a108d722f src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Fri Jul 12 21:13:57 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Fri Jul 12 21:14:54 2013 +0200
@@ -125,7 +125,9 @@
               SimpM => Simplifier.asm_full_simp_tac
             | AutoM => (fn ctxt => K (Clasimp.auto_tac ctxt))
             | 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
 
 
diff -r fe411c1dc180 -r 564a108d722f src/HOL/Tools/Sledgehammer/sledgehammer_print.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Fri Jul 12 21:13:57 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Fri Jul 12 21:14:54 2013 +0200
@@ -175,7 +175,9 @@
         SimpM => "simp"
       | AutoM => "auto"
       | FastforceM => "fastforce"
+      | ForceM => "force"
       | ArithM => "arith"
+      | Blast => "blast"
       | _ => raise Fail "Sledgehammer_Print: by_method")
 
     fun using_facts [] [] = ""
diff -r fe411c1dc180 -r 564a108d722f src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Fri Jul 12 21:13:57 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Fri Jul 12 21:14:54 2013 +0200
@@ -29,7 +29,9 @@
     SimpM |
     AutoM |
     FastforceM |
-    ArithM
+    ForceM |
+    ArithM |
+    BlastM
 
   (* legacy *)
   val By_Metis : facts -> byline
@@ -94,7 +96,9 @@
   SimpM |
   AutoM |
   FastforceM |
-  ArithM
+  ForceM |
+  ArithM |
+  BlastM
 
 (* legacy *)
 fun By_Metis facts = By (facts, MetisM)
diff -r fe411c1dc180 -r 564a108d722f src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML	Fri Jul 12 21:13:57 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML	Fri Jul 12 21:14:54 2013 +0200
@@ -23,7 +23,7 @@
 fun variants (Let _) = raise Fail "Sledgehammer_Try0: variants"
   | variants (Prove (qs, xs, l, t, subproofs, By (facts, _))) =
       let
-        val methods = [SimpM, AutoM, FastforceM, ArithM]
+        val methods = [SimpM, FastforceM, AutoM, ArithM, ForceM, BlastM]
         fun step method = Prove (qs, xs, l, t, subproofs, By (facts, method))
         (*fun step_without_facts method =
           Prove (qs, xs, l, t, subproofs, By (no_facts, method))*)
diff -r fe411c1dc180 -r 564a108d722f src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jul 12 21:13:57 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jul 12 21:14:54 2013 +0200
@@ -4,8 +4,6 @@
 General-purpose functions used by the Sledgehammer modules.
 *)
 
-infix 1 |>! #>!
-
 signature SLEDGEHAMMER_UTIL =
 sig
   val sledgehammerN : string
@@ -33,12 +31,6 @@
   val max : ('a * 'a -> order) -> 'a -> 'a -> 'a
   val max_option : ('a * 'a -> order) -> 'a option -> 'a option -> 'a option
   val max_list : ('a * 'a -> order) -> 'a list -> 'a option
-
-  (** debugging **)
-  val print_timing : ('a -> 'b) -> 'a -> 'b
-  (* infix versions of print_timing; meant to replace '|>' and '#>' *)
-  val |>! : 'a * ('a -> 'b) -> 'b
-  val #>! : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c
 end;
 
 structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
@@ -173,14 +165,4 @@
 
 fun max_list ord xs = fold (SOME #> max_option ord) xs NONE
 
-(** debugging **)
-fun print_timing f x =
-  Timing.timing f x
-  |>> Timing.message
-  |>> warning
-  |> snd
-
-fun x |>! f = print_timing f x
-fun (f #>! g) x = x |> f |>! g
-
 end;