--- a/Nominal/nominal_dt_rawfuns.ML	Tue Jul 27 09:09:02 2010 +0200
+++ b/Nominal/nominal_dt_rawfuns.ML	Tue Jul 27 14:37:59 2010 +0200
@@ -213,8 +213,6 @@
 
 fun define_raw_fvs descr sorts bn_info bclausesss constr_thms lthy =
 let
-  val _ = tracing ("bclausesss\n" ^ cat_lines (map (cat_lines o map PolyML.makestring) bclausesss))
-
   val fv_names = prefix_dt_names descr sorts "fv_"
   val fv_arg_tys = all_dtyps descr sorts
   val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys;