author | bulwahn |
Fri, 11 Mar 2011 08:58:29 +0100 | |
changeset 41904 | 2ae19825f7b6 |
parent 41903 | 39fd77f0ae59 |
child 41905 | e2611bc96022 |
--- 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