diff -r 25dcb2b1329e -r 515e5496171c Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Mon Dec 06 14:24:17 2010 +0000
+++ b/Nominal/Nominal2.thy	Mon Dec 06 16:35:42 2010 +0000
@@ -265,8 +265,6 @@
     then define_raw_dts dts bn_funs bn_eqs bclauses lthy
     else raise TEST lthy
 
-  val _ = tracing ("raw_bn_funs\n" ^ cat_lines (map (@{make_string} o #1) raw_bn_funs))
- 
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names)
   val {descr, sorts, ...} = dtinfo
 
@@ -309,12 +307,6 @@
       (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3
     else raise TEST lthy3
 
-  (*
-  val _ = tracing ("RAW_BNS\n" ^ cat_lines (map (Syntax.string_of_term lthy3) raw_bns))
-  val _ = tracing ("RAW_BN_INFO\n" ^ cat_lines (map (Syntax.string_of_term lthy3 o #1) raw_bn_info))
-  val _ = tracing ("RAW_BN_INFO\n" ^ cat_lines (map @{make_string} raw_bn_info))
-  *)
-
   (* defining the permute_bn functions *)
   val (raw_perm_bns, raw_perm_bn_simps, lthy3b) = 
     if get_STEPS lthy3a > 2
@@ -493,14 +485,6 @@
   val qalpha_bns_descr = 
     map2 (fn (b, _, _) => fn t => ("alpha_" ^ Name.of_binding b, t, NoSyn)) bn_funs  alpha_bn_trms
 
-  (*
-  val _ = tracing ("raw_bn_info\n" ^ cat_lines (map (Syntax.string_of_term lthy7 o #1) raw_bn_info))
-  val _ = tracing ("bn_funs\n" ^ cat_lines (map (@{make_string} o #1) bn_funs))
-  val _ = tracing ("raw_bns\n" ^ cat_lines (map (Syntax.string_of_term lthy7) raw_bns))
-  val _ = tracing ("raw_fv_bns\n" ^ cat_lines (map (Syntax.string_of_term lthy7) raw_fv_bns))
-  val _ = tracing ("alpha_bn_trms\n" ^ cat_lines (map (Syntax.string_of_term lthy7) alpha_bn_trms))
-  *)
-
   val qperm_descr =
     map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn)) qty_names raw_perm_funs
 
@@ -559,7 +543,7 @@
       ||>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt)
     else raise TEST lthy9a
 
-  val (((((qsize_eqvt, [qinduct]), qexhausts), qsize_simps), qperm_bn_simps), lthyB) = 
+  val ((((((qsize_eqvt, [qinduct]), qexhausts), qsize_simps), qperm_bn_simps), qalpha_refl_thms), lthyB) = 
     if get_STEPS lthy > 28
     then
       lthyA 
@@ -568,6 +552,7 @@
       ||>> lift_thms qtys [] raw_exhaust_thms
       ||>> lift_thms qtys [] raw_size_thms
       ||>> lift_thms qtys [] raw_perm_bn_simps
+      ||>> lift_thms qtys [] alpha_refl_thms
     else raise TEST lthyA
 
   val qinducts = Project_Rule.projections lthyA qinduct
@@ -626,11 +611,11 @@
     else []
 
   (* proving that perm_bns preserve alpha *)
-  val qperm_bn_alpha_thms = @{thms TrueI}
-  (*  if get_STEPS lthy > 33
-    then prove_perm_bn_alpha_thms qtys qperm_bns qalpha_bns qinduct qperm_bn_simps qeq_iffs' lthyC
-    else []*)
-
+  val qperm_bn_alpha_thms = 
+    if get_STEPS lthy > 33
+    then prove_perm_bn_alpha_thms qtys qperm_bns qalpha_bns qinduct qperm_bn_simps qeq_iffs' 
+      qalpha_refl_thms lthyC
+    else []
 
   (* noting the theorems *)