diff -r dd3b9c046c7d -r 4da5c5c29009 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Thu Jun 03 15:02:52 2010 +0200
+++ b/Nominal/NewParser.thy	Mon Jun 07 11:43:01 2010 +0200
@@ -405,18 +405,33 @@
  
   val lthy_tmp' = snd (Local_Theory.note ((Binding.empty, [add_eqvt]), fv_eqvt) lthy_tmp)
 
-  val (alpha_eqvt, _) =
+  val (alpha_eqvt, lthy_tmp'') =
     if get_STEPS lthy > 8
-    then Nominal_Eqvt.equivariance false alpha_trms alpha_induct alpha_intros lthy_tmp'
+    then Nominal_Eqvt.equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy_tmp'
+    else raise TEST lthy4
+
+  (* proving alpha equivalence *)
+  val _ = warning "Proving equivalence"
+
+  val alpha_sym_thms = 
+    if get_STEPS lthy > 9
+    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
+    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
+
+
+  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 _ = 
-    if get_STEPS lthy > 9
+    if get_STEPS lthy > 11
     then true else raise TEST lthy4
 
-  (* proving alpha equivalence *)
-  val _ = warning "Proving equivalence";
-
   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;
@@ -424,6 +439,7 @@
     if !cheat_equivp then map (equivp_hack lthy4) alpha_trms
     else build_equivps alpha_trms reflps alpha_induct
       inject_thms alpha_eq_iff distinct_thms alpha_cases alpha_eqvt lthy4;
+
   val qty_binds = map (fn (_, b, _, _) => b) dts;
   val qty_names = map Name.of_binding qty_binds;
   val qty_full_names = map (Long_Name.qualify thy_name) qty_names