--- a/Nominal/NewParser.thy	Thu Jun 10 14:53:45 2010 +0200
+++ b/Nominal/NewParser.thy	Fri Jun 11 03:02:42 2010 +0200
@@ -326,7 +326,7 @@
 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
 let
   (* definition of the raw datatypes *)
-
+  val _ = warning "Definition of raw datatypes";
   val (dt_names, raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) =
     if get_STEPS lthy > 0 
     then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
@@ -347,6 +347,7 @@
   val exhaust_thms = map #exhaust dtinfos;
 
   (* definitions of raw permutations *)
+  val _ = warning "Definition of raw permutations";
   val ((raw_perm_funs, raw_perm_defs, raw_perm_simps), lthy2) =
     if get_STEPS lthy0 > 1 
     then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy0
@@ -360,6 +361,7 @@
   val thy_name = Context.theory_name thy
 
   (* definition of raw fv_functions *)
+  val _ = warning "Definition of raw fv-functions";
   val lthy3 = Theory_Target.init NONE thy;
 
   val (raw_bn_funs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) =
@@ -367,25 +369,25 @@
     then raw_bn_decls dt_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3
     else raise TEST lthy3
 
-  val bn_nos = map (fn (_, i, _) => i) raw_bn_info;
-  val bns = raw_bn_funs ~~ bn_nos;
-
   val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) = 
     if get_STEPS lthy3a > 3 
     then define_raw_fvs descr sorts raw_bn_info raw_bclauses constr_thms lthy3a
     else raise TEST lthy3a
 
   (* definition of raw alphas *)
+  val _ = warning "Definition of alphas";
   val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) =
     if get_STEPS lthy3b > 4 
     then define_raw_alpha descr sorts raw_bn_info raw_bclauses raw_fvs lthy3b
     else raise TEST lthy3b
   
   (* definition of alpha-distinct lemmas *)
+  val _ = warning "Distinct theorems";
   val (alpha_distincts, alpha_bn_distincts) = 
     mk_alpha_distincts lthy4 alpha_cases raw_constrs_distinct alpha_trms alpha_bn_trms raw_bn_info
 
   (* definition of raw_alpha_eq_iff  lemmas *)
+  val _ = warning "Eq-iff theorems";
   val alpha_eq_iff = 
     if get_STEPS lthy > 5
     then mk_alpha_eq_iff lthy4 alpha_intros distinct_thms inject_thms alpha_cases
@@ -418,13 +420,18 @@
   (* proving alpha equivalence *)
   val _ = warning "Proving equivalence"
 
+  val alpha_refl_thms = 
+    if get_STEPS lthy > 9
+    then raw_prove_refl alpha_trms alpha_bn_trms alpha_intros induct_thm lthy_tmp'' 
+    else raise TEST lthy4
+
   val alpha_sym_thms = 
-    if get_STEPS lthy > 9
+    if get_STEPS lthy > 10
     then raw_prove_sym (alpha_trms @ alpha_bn_trms) alpha_intros alpha_induct lthy_tmp'' 
     else raise TEST lthy4
 
   val alpha_trans_thms = 
-    if get_STEPS lthy > 10
+    if get_STEPS lthy > 11
     then raw_prove_trans (alpha_trms @ alpha_bn_trms) (distinct_thms @ inject_thms) 
            alpha_intros alpha_induct alpha_cases lthy_tmp'' 
     else raise TEST lthy4
@@ -432,13 +439,16 @@
 
   val _ = tracing ("alphas " ^ commas (map (Syntax.string_of_term lthy4) alpha_trms))
   val _ = tracing ("alpha_bns " ^ commas (map (Syntax.string_of_term lthy4) alpha_bn_trms))
-  val _ = tracing ("alpha_trans\n" ^ 
-    cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_trans_thms))
+  val _ = tracing ("alpha_refl\n" ^ 
+    cat_lines (map (Syntax.string_of_term lthy4 o prop_of) alpha_refl_thms))
 
   val _ = 
-    if get_STEPS lthy > 11
+    if get_STEPS lthy > 12
     then true else raise TEST lthy4
 
+  val bn_nos = map (fn (_, i, _) => i) raw_bn_info;
+  val bns = raw_bn_funs ~~ bn_nos;
+
   val fv_alpha_all = combine_fv_alpha_bns (raw_fvs, raw_fv_bns) (alpha_trms, alpha_bn_trms) bn_nos
 
   val reflps = build_alpha_refl fv_alpha_all alpha_trms induct_thm alpha_eq_iff lthy4;