--- a/Nominal/nominal_function.ML	Thu Jun 16 12:12:25 2011 +0100
+++ b/Nominal/nominal_function.ML	Thu Jun 16 13:14:16 2011 +0100
@@ -45,8 +45,6 @@
 (* Check for all sorts of errors in the input - nominal needs a different checking function *)
 fun nominal_check_defs ctxt fixes eqs =
   let
-    val _ = tracing ("fixes: " ^ @{make_string} fixes)
-
     val fnames = map (fst o fst) fixes
 
     fun check geq =