# HG changeset patch
# User blanchet
# Date 1301992631 -7200
# Node ID 5f2a555b15d69ff2639539b9a731b45450995c7e
# Parent  bc1891226d00a72219827ce9affbdc9d85d0a26a
remove debugging code

diff -r bc1891226d00 -r 5f2a555b15d6 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue Apr 05 09:38:28 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue Apr 05 10:37:11 2011 +0200
@@ -433,7 +433,6 @@
            (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
                                                 quote s)) parse_mangled_type))
     |> fst
-    |> tap (fn u => PolyML.makestring u |> warning) (*###*)
 
 fun unmangled_const s =
   let val ss = space_explode mangled_type_sep s in