# HG changeset patch
# User smolkas
# Date 1373653714 -7200
# Node ID 94fbc50a6757ee4bdb3564ce6c2177b62ea08656
# Parent  ecb4a858991d8da9d2903f44064485632ffe8856
removed |>! and #>!

diff -r ecb4a858991d -r 94fbc50a6757 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jul 12 19:54:36 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Jul 12 20:28:34 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;