--- a/Nominal/nominal_dt_rawfuns.ML	Mon Jul 26 09:19:28 2010 +0200
+++ b/Nominal/nominal_dt_rawfuns.ML	Tue Jul 27 09:09:02 2010 +0200
@@ -213,6 +213,8 @@
 
 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;