| changeset 20405 | 8276fd8d1919 |
| parent 20389 | 8b6ecb22ef35 |
| child 20428 | 67fa1c6ba89e |
--- a/src/Pure/Tools/codegen_thingol.ML Mon Aug 21 11:02:43 2006 +0200 +++ b/src/Pure/Tools/codegen_thingol.ML Mon Aug 21 11:02:44 2006 +0200 @@ -116,7 +116,7 @@ (** auxiliary **) val debug = ref false; -fun debug_msg f x = (if !debug then Output.debug (f x) else (); x); +fun debug_msg f x = (if !debug then Output.tracing (f x) else (); x); val soft_exc = ref true; fun unfoldl dest x =