--- a/Nominal/Fv.thy	Tue Mar 16 17:20:46 2010 +0100
+++ b/Nominal/Fv.thy	Tue Mar 16 18:18:08 2010 +0100
@@ -210,11 +210,10 @@
   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
   val alpha_bn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn)));
   val alpha_bn_type = 
-    if is_rec then @{typ perm} --> nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool}
-    else nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool};
+    (*if is_rec then @{typ perm} --> nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool} else*)
+    nth_dtyp ith_dtyp --> nth_dtyp ith_dtyp --> @{typ bool};
   val alpha_bn_free = Free(alpha_bn_name, alpha_bn_type);
   val pi = Free("pi", @{typ perm})
-  val alpha_bn_pi = if is_rec then alpha_bn_free $ pi else alpha_bn_free;
   fun alpha_bn_constr (cname, dts) args_in_bn =
   let
     val Ts = map (typ_of_dtyp descr sorts) dts;
@@ -224,19 +223,18 @@
     val args2 = map Free (names2 ~~ Ts);
     val c = Const (cname, Ts ---> (nth_dtyp ith_dtyp));
     val rhs = HOLogic.mk_Trueprop
-      (alpha_bn_pi $ (list_comb (c, args)) $ (list_comb (c, args2)));
+      (alpha_bn_free $ (list_comb (c, args)) $ (list_comb (c, args2)));
     fun lhs_arg ((dt, arg_no), (arg, arg2)) =
       let
         val argty = fastype_of arg;
         val permute = Const (@{const_name permute}, @{typ perm} --> argty --> argty);
-        val permarg = if is_rec then permute $ pi $ arg else arg
       in
       if is_rec_type dt then
-        if arg_no mem args_in_bn then alpha_bn_pi $ arg $ arg2
-        else (nth alpha_frees (body_index dt)) $ permarg $ arg2
+        if arg_no mem args_in_bn then alpha_bn_free $ arg $ arg2
+        else (nth alpha_frees (body_index dt)) $ arg $ arg2
       else
         if arg_no mem args_in_bn then @{term True}
-        else HOLogic.mk_eq (permarg, arg2)
+        else HOLogic.mk_eq (arg, arg2)
       end
     val arg_nos = 0 upto (length dts - 1)
     val lhss = mk_conjl (map lhs_arg (dts ~~ arg_nos ~~ (args ~~ args2)))
@@ -355,19 +353,31 @@
               else (HOLogic.mk_eq (arg, arg2))
           | (_, [], []) => @{term True}
           | ([], ((((SOME (bn, is_rec)), _, _), pi) :: _), []) =>
-            let
-              val alpha_bn_const =
-                nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns)
-              val alpha_bn =
-                if is_rec then alpha_bn_const $ pi $ arg $ arg2 else alpha_bn_const $ arg $ arg2
-              val ty = fastype_of (bn $ arg)
-              val permute = Const(@{const_name permute}, @{typ perm} --> ty --> ty)
-            in
-              if bns_same rel_in_comp_binds then
-                alpha_bn
-(*                HOLogic.mk_conj (alpha_bn, HOLogic.mk_eq (permute $ pi $ (bn $ arg), (bn $ arg2)))*)
-              else error "incompatible bindings for one argument"
-            end
+            if not (bns_same rel_in_comp_binds) then error "incompatible bindings for an argument" else
+            if is_rec then
+              let
+                val (rbinds, rpis) = split_list rel_in_comp_binds
+                val lhs_binds = fv_binds args rbinds
+                val lhs = mk_pair (lhs_binds, arg);
+                val rhs_binds = fv_binds args2 rbinds;
+                val rhs = mk_pair (rhs_binds, arg2);
+                val alpha = nth alpha_frees (body_index dt);
+                val fv = nth fv_frees (body_index dt);
+                val pi = foldr1 add_perm (distinct (op =) rpis);
+                val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs;
+                val alpha_gen = Syntax.check_term lthy alpha_gen_pre
+              in
+                alpha_gen
+              end
+            else
+              let
+                val alpha_bn_const =
+                  nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns)
+                val ty = fastype_of (bn $ arg)
+                val permute = Const(@{const_name permute}, @{typ perm} --> ty --> ty)
+              in
+                alpha_bn_const $ arg $ arg2
+              end
           | ([], [], relevant) =>
             let
               val (rbinds, rpis) = split_list relevant
@@ -380,10 +390,7 @@
               val pi = foldr1 add_perm (distinct (op =) rpis);
               val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs;
               val alpha_gen = Syntax.check_term lthy alpha_gen_pre
-(*              val pi_supps = map ((curry op $) @{term "supp :: perm \<Rightarrow> atom set"}) rpis;
-              val pi_supps_eq = HOLogic.mk_eq (mk_inter pi_supps, @{term "{} :: atom set"}) *)
             in
-(*              if length pi_supps > 1 then HOLogic.mk_conj (alpha_gen, pi_supps_eq) else*)
               alpha_gen
             end
           | _ => error "Fv.alpha: not supported binding structure"