--- a/Nominal/nominal_dt_alpha.ML	Fri Aug 27 02:08:36 2010 +0800
+++ b/Nominal/nominal_dt_alpha.ML	Fri Aug 27 03:37:17 2010 +0800
@@ -29,7 +29,7 @@
     term list -> thm -> thm list -> Proof.context -> thm list
   val raw_size_rsp_aux: term list -> thm -> thm list -> Proof.context -> thm list
   val raw_constrs_rsp: term list -> term list -> thm list -> thm list -> Proof.context -> thm list
-  val raw_alpha_bn_rsp: thm list -> thm list -> thm list
+  val raw_alpha_bn_rsp: term list -> thm list -> thm list -> thm list
 
   val mk_funs_rsp: thm -> thm
   val mk_alpha_permute_rsp: thm -> thm 
@@ -703,12 +703,25 @@
   @{lemma "[|equivp Q; !!x y. R x y ==> Q x y|] ==> (R ===> R ===> op =) Q Q"
     by (simp only: fun_rel_def equivp_def, metis)}
 
-fun raw_alpha_bn_rsp alpha_bn_equivp alpha_bn_imps =
+
+(* we have to reorder the alpha_bn_imps theorems in order
+   to be in order with alpha_bn_trms *)
+fun raw_alpha_bn_rsp alpha_bn_trms alpha_bn_equivp alpha_bn_imps =
 let
+  fun mk_map thm =
+    thm |> `prop_of
+        |>> List.last  o snd o strip_comb
+        |>> HOLogic.dest_Trueprop
+        |>> head_of
+        |>> fst o dest_Const
+
+  val alpha_bn_imps' = 
+    map (lookup (map mk_map alpha_bn_imps) o fst o dest_Const) alpha_bn_trms
+
   fun mk_thm thm1 thm2 = 
     (forall_intr_vars thm2) COMP (thm1 RS rsp_equivp)
 in
-  map2 mk_thm alpha_bn_equivp alpha_bn_imps
+  map2 mk_thm alpha_bn_equivp alpha_bn_imps'
 end