src/HOL/Tools/smallvalue_generators.ML
changeset 41904 2ae19825f7b6
parent 41903 39fd77f0ae59
--- a/src/HOL/Tools/smallvalue_generators.ML	Fri Mar 11 08:13:00 2011 +0100
+++ b/src/HOL/Tools/smallvalue_generators.ML	Fri Mar 11 08:58:29 2011 +0100
@@ -340,7 +340,6 @@
   
 fun post_process_term t =
   let
-    val _ = tracing (Syntax.string_of_term @{context} t)
     fun map_Abs f t =
       case t of Abs (x, T, t') => Abs (x, T, f t') | _ => raise TERM ("map_Abs", [t]) 
     fun process_args t = case strip_comb t of