diff -r 39ae45d3a11b -r 2b8e387d2dfc Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Thu Jun 16 23:11:50 2011 +0900
+++ b/Nominal/Nominal2.thy	Thu Jun 16 20:07:03 2011 +0100
@@ -261,43 +261,45 @@
      
   val lthy5 = snd (Local_Theory.note ((Binding.empty, [eqvt_attr]), raw_fv_eqvt) lthy_tmp)
 
-  val (alpha_eqvt, lthy6) =
-    Nominal_Eqvt.raw_equivariance true (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5
+  val alpha_eqvt =
+    Nominal_Eqvt.raw_equivariance (alpha_trms @ alpha_bn_trms) alpha_induct alpha_intros lthy5
+
+  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 lthy6 
+    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 lthy6 
+    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 lthy6
+      alpha_intros alpha_induct alpha_cases alpha_eqvt_norm lthy5
 
   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 lthy6
+      alpha_trans_thms lthy5
 
   val _ = trace_msg (K "Proving alpha implies bn...")
   val alpha_bn_imp_thms = 
-    raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy6 
+    raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy5 
   
   val _ = trace_msg (K "Proving respectfulness...")
   val raw_funs_rsp_aux = 
     raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs 
-      raw_bns raw_fv_bns alpha_induct (raw_bn_defs @ raw_fv_defs) lthy6
+      raw_bns raw_fv_bns alpha_induct (raw_bn_defs @ raw_fv_defs) lthy5
   
   val raw_funs_rsp = map mk_funs_rsp raw_funs_rsp_aux
 
   val raw_size_rsp = 
     raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct 
-      (raw_size_thms @ raw_size_eqvt) lthy6
+      (raw_size_thms @ raw_size_eqvt) lthy5
       |> map mk_funs_rsp
 
   val raw_constrs_rsp = 
     raw_constrs_rsp (flat raw_constrs) alpha_trms alpha_intros
-      (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy6 
+      (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy5 
     
   val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt
 
@@ -306,19 +308,19 @@
 
   val raw_perm_bn_rsp =
     raw_perm_bn_rsp (alpha_trms @ alpha_bn_trms) raw_perm_bns alpha_induct 
-      alpha_intros raw_perm_bn_simps lthy6
+      alpha_intros raw_perm_bn_simps lthy5
 
   (* noting the quot_respects lemmas *)
-  val (_, lthy6a) = 
+  val (_, lthy6) = 
     Local_Theory.note ((Binding.empty, [rsp_attr]),
       raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ 
-      alpha_bn_rsp @ raw_perm_bn_rsp) lthy6
+      alpha_bn_rsp @ raw_perm_bn_rsp) lthy5
 
   val _ = trace_msg (K "Defining the quotient types...")
   val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts
      
   val (qty_infos, lthy7) = 
-    define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6a
+    define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6
 
   val qtys = map #qtyp qty_infos
   val qty_full_names = map (fst o dest_Type) qtys