src/HOL/Tools/smallvalue_generators.ML

   | make_map T1 T2 ((_, Const (@{const_name None}, _)) :: tps) = make_map T1 T2 tps
   | make_map T1 T2 ((t1, t2) :: tps) = mk_fun_upd T1 T2 (t1, t2) (make_map T1 T2 tps)
   
 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
       (c as Const (_, _), ts) => list_comb (c, map post_process_term ts) 
   in