--- a/Nominal/Nominal2.thy	Thu Jan 06 20:25:40 2011 +0000
+++ b/Nominal/Nominal2.thy	Thu Jan 06 23:06:45 2011 +0000
@@ -167,7 +167,6 @@
 ML {*
 fun nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses lthy =
 let
-  (* definition of the raw datatypes *)
   val _ = trace_msg (K "Defining raw datatypes...")
   val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, cnstr_names, lthy0) =
     define_raw_dts dts bn_funs bn_eqs bclauses lthy   
@@ -203,7 +202,6 @@
   (* noting the raw permutations as eqvt theorems *)
   val (_, lthy3) = Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_perm_simps) lthy2a
 
-
   val _ = trace_msg (K "Defining raw fv- and bn-functions...")
   val (raw_bns, raw_bn_defs, raw_bn_info, raw_bn_induct, lthy3a) =
     define_raw_bns raw_full_ty_names raw_dts raw_bn_funs raw_bn_eqs 
@@ -362,8 +360,7 @@
   val qalpha_bns = map #qconst qalpha_bns_info
   val qperm_bns = map #qconst qperm_bns_info
 
-  val _ = trace_msg (K "Lifting of theorems...")
-  
+  val _ = trace_msg (K "Lifting of theorems...")  
   val eq_iff_simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel_def
     prod.cases} 
 
@@ -403,7 +400,6 @@
       qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC
 
   (* postprocessing of eq and fv theorems *)
-
   val qeq_iffs' = qeq_iffs
     |> map (simplify (HOL_basic_ss addsimps qfv_supp_thms))
     |> map (simplify (HOL_basic_ss addsimps @{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]}))