--- a/Nominal/Nominal2.thy	Wed Jun 29 19:21:26 2011 +0100
+++ b/Nominal/Nominal2.thy	Wed Jun 29 23:08:44 2011 +0100
@@ -232,7 +232,7 @@
       (raw_inject_thms @ raw_distinct_thms) raw_size_thms lthy3b
     
   val _ = trace_msg (K "Defining alpha relations...")
-  val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy4) =
+  val (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, alpha_result, lthy4) =
     define_raw_alpha raw_dt_names raw_tys raw_cns_info raw_bn_info raw_bclauses raw_fvs lthy3c
     
   val _ = tracing ("alpha_induct\n" ^ Syntax.string_of_term lthy3c (prop_of alpha_induct))
@@ -242,11 +242,10 @@
 
   val _ = trace_msg (K "Proving distinct theorems...")
   val alpha_distincts = 
-    raw_prove_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_dt_names
+    raw_prove_alpha_distincts lthy4 alpha_result raw_distinct_thms raw_dt_names
 
   val _ = trace_msg (K "Proving eq-iff theorems...")
-  val alpha_eq_iff = 
-    raw_prove_alpha_eq_iff lthy4 alpha_intros raw_distinct_thms raw_inject_thms alpha_cases
+  val alpha_eq_iff = raw_prove_alpha_eq_iff lthy4 alpha_result raw_distinct_thms raw_inject_thms
     
   val _ = trace_msg (K "Proving equivariance of bns, fvs, size and alpha...")
   val raw_bn_eqvt = 
@@ -273,19 +272,13 @@
   val alpha_eqvt_norm = map (Nominal_ThmDecls.eqvt_transform lthy5) alpha_eqvt
 
   val _ = trace_msg (K "Proving equivalence of alpha...")
-  val alpha_refl_thms = 
-    raw_prove_refl alpha_trms alpha_bn_trms alpha_intros raw_induct_thm lthy5 
-
-  val alpha_sym_thms = 
-    raw_prove_sym (alpha_trms @ alpha_bn_trms) alpha_intros alpha_induct alpha_eqvt_norm lthy5 
-
-  val alpha_trans_thms = 
-    raw_prove_trans (alpha_trms @ alpha_bn_trms) (raw_distinct_thms @ raw_inject_thms) 
-      alpha_intros alpha_induct alpha_cases alpha_eqvt_norm lthy5
+  val alpha_refl_thms = raw_prove_refl lthy5 alpha_result raw_induct_thm  
+  val alpha_sym_thms = raw_prove_sym lthy5 alpha_result alpha_eqvt_norm
+  val alpha_trans_thms =
+    raw_prove_trans lthy5 alpha_result (raw_distinct_thms @ raw_inject_thms) alpha_eqvt_norm
 
   val (alpha_equivp_thms, alpha_bn_equivp_thms) = 
-    raw_prove_equivp alpha_trms alpha_bn_trms alpha_refl_thms alpha_sym_thms 
-      alpha_trans_thms lthy5
+    raw_prove_equivp lthy5 alpha_result alpha_refl_thms alpha_sym_thms alpha_trans_thms
 
   val _ = trace_msg (K "Proving alpha implies bn...")
   val alpha_bn_imp_thms =