--- a/Nominal/Fv.thy	Thu Mar 18 15:13:20 2010 +0100
+++ b/Nominal/Fv.thy	Thu Mar 18 15:32:49 2010 +0100
@@ -94,21 +94,39 @@
 
 2) alpha_ty relations are generated for all the types being defined:
 
-   !!! permutations !!!
+   For each constructor we gather all the arguments that are bound,
+   and for each of those we add a permutation. We associate those
+   permutations with the bindings. Note that two bindings can have
+   the same permutation if the arguments being bound are the same.
 
-   An alpha_ty for a constructor is true if a conjunction of
-   propositions for each argument holds.
+   An alpha_ty for a constructor is true if there exist permutations
+   as above such that a conjunction of propositions for all arguments holds.
 
    For an argument we allow bindings where only one of the following
    holds:
 
    - Argument is bound in some shallow bindings: We return true
-   - Argument is bound in some deep recursive bindings
-     !!! still to describe !!!
+   - Argument of type ty is bound recursively in some other
+     arguments [i1, .. in] with one binding function bn.
+     We return:
+
+     (bn argl, (argl, argl_i1, ..., argl_in)) \<approx>gen
+     \<lambda>(argl,argl1,..,argln) (argr,argr1,..,argrn). 
+         (alpha_ty argl argr) \<and> (alpha_i1 argl1 argr1) \<and> .. \<and> (alpha_in argln argrn)
+     \<lambda>(arg,arg1,..,argn). (fv_ty arg) \<union> (fv_i1 arg1) \<union> .. \<union> (fv_in argn)
+     pi
+     (bn argr, (argr, argr_i1, ..., argr_in))
+
    - Argument is bound in some deep non-recursive bindings.
      We return: alpha_bn argl argr
-   - Argument has some shallow and/or non-recursive bindings.
-     !!! still to describe !!!
+   - Argument of type ty has some shallow bindings [b1..bn] and/or
+     non-recursive bindings [f1 a1, .., fm am], where the bindings
+     have the permutations p1..pl. We return:
+
+     (b1l \<union>..\<union> bnl \<union> f1 a1l \<union>..\<union> fn anl, argl) \<approx>gen
+     alpha_ty fv_ty (p1 +..+ pl)
+     (b1r \<union>..\<union> bnr \<union> f1 a1r \<union>..\<union> fn anr, argr)
+
    - Argument has some recursive bindings. The bindings were
      already treated in 2nd case so we return: True
    - Argument has no bindings and is not bound.
@@ -461,8 +479,6 @@
               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

--- a/TODO	Thu Mar 18 15:13:20 2010 +0100
+++ b/TODO	Thu Mar 18 15:32:49 2010 +0100
@@ -1,8 +1,5 @@
 Smaller things:
 
-- case names for "weak" induction rules (names of the 
-constructors); see page 61/62 and 170 in Tutorial
-
 - maybe <type>_perm whould be called permute_<type>.simps;
   that would conform with the terminology in Nominal2