--- a/Nominal/Fv.thy	Sat Mar 27 06:44:16 2010 +0100
+++ b/Nominal/Fv.thy	Sat Mar 27 06:51:13 2010 +0100
@@ -136,14 +136,18 @@
 *)
 
 ML {*
+datatype alpha_type = AlphaGen | AlphaRes | AlphaLst;
+*}
+
+ML {*
 fun is_atom thy typ =
   Sign.of_sort thy (typ, @{sort at})
 
 fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t
-  | is_atom_set thy _ = false;
+  | is_atom_set _ _ = false;
 
 fun is_atom_fset thy (Type ("FSet.fset", [t])) = is_atom thy t
-  | is_atom_fset thy _ = false;
+  | is_atom_fset _ _ = false;
 *}
 
 
@@ -326,11 +330,10 @@
 
 
 ML {*
-fun alpha_bn thy (dt_info : Datatype_Aux.info) alpha_frees bn_alphabn ((bn, ith_dtyp, args_in_bns), (alpha_bn_free, is_rec)) =
+fun alpha_bn (dt_info : Datatype_Aux.info) alpha_frees bn_alphabn ((bn, ith_dtyp, args_in_bns), (alpha_bn_free, _ (*is_rec*) )) =
 let
   val {descr, sorts, ...} = dt_info;
   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
-  val pi = Free("pi", @{typ perm})
   fun alpha_bn_constr (cname, dts) args_in_bn =
   let
     val Ts = map (typ_of_dtyp descr sorts) dts;
@@ -342,17 +345,12 @@
     val rhs = HOLogic.mk_Trueprop
       (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);
-      in
-        case AList.lookup (op=) args_in_bn arg_no of
-          SOME NONE => @{term True}
-        | SOME (SOME f) => (the (AList.lookup (op=) bn_alphabn f)) $ arg $ arg2
-        | NONE =>
-            if is_rec_type dt then (nth alpha_frees (body_index dt)) $ arg $ arg2
-            else HOLogic.mk_eq (arg, arg2)
-      end
+      case AList.lookup (op=) args_in_bn arg_no of
+        SOME NONE => @{term True}
+      | SOME (SOME f) => (the (AList.lookup (op=) bn_alphabn f)) $ arg $ arg2
+      | NONE =>
+          if is_rec_type dt then (nth alpha_frees (body_index dt)) $ arg $ arg2
+          else HOLogic.mk_eq (arg, arg2)
     val arg_nos = 0 upto (length dts - 1)
     val lhss = mk_conjl (map lhs_arg (dts ~~ arg_nos ~~ (args ~~ args2)))
     val eq = Logic.mk_implies (HOLogic.mk_Trueprop lhss, rhs)
@@ -367,7 +365,7 @@
 *}
 
 ML {*
-fun alpha_bns thy dt_info alpha_frees rel_bns bns_rec =
+fun alpha_bns dt_info alpha_frees rel_bns bns_rec =
 let
   val {descr, sorts, ...} = dt_info;
   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
@@ -381,7 +379,7 @@
     end;
   val (alphabn_names, alphabn_frees) = split_list (map mk_alphabn_free rel_bns);
   val bn_alphabn = (map (fn (bn, _, _) => bn) rel_bns) ~~ alphabn_frees;
-  val pair = split_list (map (alpha_bn thy dt_info alpha_frees bn_alphabn)
+  val pair = split_list (map (alpha_bn dt_info alpha_frees bn_alphabn)
     (rel_bns ~~ (alphabn_frees ~~ bns_rec)))
 in
   (alphabn_names, pair)
@@ -422,7 +420,7 @@
   (* We assume that a bn is either recursive or not *)
   val bns_rec = map (fn (bn, _, _) => not (bn mem nr_bns)) bns;
   val (alpha_bn_names, (bn_alpha_bns, alpha_bn_eqs)) =
-    alpha_bns thy dt_info alpha_frees bns bns_rec
+    alpha_bns dt_info alpha_frees bns bns_rec
   val alpha_bn_frees = map snd bn_alpha_bns;
   val alpha_bn_types = map fastype_of alpha_bn_frees;
   fun fv_alpha_constr ith_dtyp (cname, dts) bindcs =
@@ -495,7 +493,7 @@
               else (HOLogic.mk_eq (arg, arg2))
           | (_, [], [], []) => @{term True}
           | ([], [], [], _) => @{term True}
-          | ([], ((((SOME (bn, is_rec)), _, _), pi) :: _), [], []) =>
+          | ([], ((((SOME (bn, is_rec)), _, _), _) :: _), [], []) =>
             if not (bns_same rel_in_comp_binds) then error "incompatible bindings for an argument" else
             if is_rec then
               let
@@ -504,7 +502,6 @@
                 val bound_in_ty_nos = map (fn i => body_index (nth dts i)) bound_in_nos;
                 val bound_args = arg :: map (nth args) bound_in_nos;
                 val bound_args2 = arg2 :: map (nth args2) bound_in_nos;
-                fun bound_in args (_, _, i) = nth args i;
                 val lhs_binds = fv_binds args rbinds
                 val lhs_arg = foldr1 HOLogic.mk_prod bound_args
                 val lhs = mk_pair (lhs_binds, lhs_arg);
@@ -578,7 +575,6 @@
      (alpha_types @ alpha_bn_types)) []
      (add_binds (alpha_eqs @ flat alpha_bn_eqs)) [] lthy'')
   val ordered_fvs = fv_frees @ fvbns;
-  val exported_fvs = map (Morphism.term (ProofContext.export_morphism lthy''' lthy)) ordered_fvs;
   val all_fvs = (fst fvs @ fst fvs2, snd fvs @ snd fvs2)
 in
   (((all_fvs, ordered_fvs), alphas), lthy''')
@@ -621,7 +617,6 @@
   val args = map Free (names ~~ tys);
   fun find_alphas ty x =
     domain_type (fastype_of x) = ty;
-  fun mk_alpha_refl arg (_, alpha) = alpha $ arg $ arg;
   fun refl_eq_arg (ty, arg) =
     let
       val rel_alphas = filter (find_alphas ty) alphas;
@@ -636,7 +631,7 @@
 *}
 
 ML {*
-fun reflp_tac induct eq_iff ctxt =
+fun reflp_tac induct eq_iff =
   rtac induct THEN_ALL_NEW
   simp_tac (HOL_basic_ss addsimps eq_iff) THEN_ALL_NEW
   split_conj_tac THEN_ALL_NEW REPEAT o rtac @{thm exI[of _ "0 :: perm"]}
@@ -649,7 +644,7 @@
 fun build_alpha_refl fv_alphas_lst alphas induct eq_iff ctxt =
 let
   val (names, gl) = build_alpha_refl_gl fv_alphas_lst alphas;
-  val refl_conj = Goal.prove ctxt names [] gl (fn _ => reflp_tac induct eq_iff ctxt 1);
+  val refl_conj = Goal.prove ctxt names [] gl (fn _ => reflp_tac induct eq_iff 1);
 in
   HOLogic.conj_elims refl_conj
 end