--- a/Nominal/NewParser.thy	Wed May 12 13:43:48 2010 +0100
+++ b/Nominal/NewParser.thy	Wed May 12 14:47:52 2010 +0100
@@ -367,11 +367,6 @@
     if STEPS > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
     else raise TEST lthy
 
-  val _ = tracing ("raw_bn_eqs\n" ^ cat_lines (map (@{make_string} o prop_of) raw_bn_eqs))
-  
-  val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns)
-  val _ = tracing ("raw_bclauses\n" ^ @{make_string} raw_bclauses)
-
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names);
   val {descr, sorts, ...} = dtinfo;
   val raw_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr;
@@ -406,12 +401,11 @@
   val lthy3 = Theory_Target.init NONE thy;
   val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls;
 
-  (*
   val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns)
   val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns_exp)
   val _ = tracing ("bn_funs\n" ^ @{make_string} bn_funs_decls)
   val _ = tracing ("raw_bclauses\n" ^ @{make_string} raw_bclauses)
-  *)
+  
   val ((fv, fvbn), fv_def, lthy3a) = 
     if STEPS > 3 then define_raw_fv descr sorts bn_funs_decls raw_bclauses lthy3
     else raise TEST lthy3