diff -r 5f2dcf15c531 -r 0ea578c6dae3 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Tue Mar 23 11:43:09 2010 +0100
+++ b/Nominal/Fv.thy	Tue Mar 23 16:28:29 2010 +0100
@@ -278,15 +278,15 @@
 end
 *}
 
+ML AList.lookup
+
 (* We assume no bindings in the type on which bn is defined *)
 (* TODO: currently works only with current fv_bn function *)
 ML {*
-fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees (bn, ith_dtyp, args_in_bns) =
+fun fv_bn thy (dt_info : Datatype_Aux.info) fv_frees bn_fvbn (fvbn, (bn, ith_dtyp, args_in_bns)) =
 let
   val {descr, sorts, ...} = dt_info;
   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
-  val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn)));
-  val fvbn = Free (fvbn_name, fastype_of (nth fv_frees ith_dtyp));
   fun fv_bn_constr (cname, dts) args_in_bn =
   let
     val Ts = map (typ_of_dtyp descr sorts) dts;
@@ -296,16 +296,18 @@
     fun fv_arg ((dt, x), arg_no) =
       let
         val ty = fastype_of x
+        val _ = tracing (PolyML.makestring args_in_bn);
+        val _ = tracing (PolyML.makestring bn_fvbn);
       in
-        if arg_no mem args_in_bn then 
-          (if is_rec_type dt then
-            (if body_index dt = ith_dtyp then fvbn $ x else error "fv_bn: recursive argument, but wrong datatype.")
-          else @{term "{} :: atom set"}) else
-        if is_atom thy ty then mk_single_atom x else
-        if is_atom_set thy ty then mk_atom_set x else
-        if is_atom_fset thy ty then mk_atom_fset x else
-        if is_rec_type dt then nth fv_frees (body_index dt) $ x else
-        @{term "{} :: atom set"}
+        case AList.lookup (op=) args_in_bn arg_no of
+          SOME NONE => @{term "{} :: atom set"}
+        | SOME (SOME (f : term)) => (the (AList.lookup (op=) bn_fvbn f)) $ x
+        | NONE =>
+            if is_atom thy ty then mk_single_atom x else
+            if is_atom_set thy ty then mk_atom_set x else
+            if is_atom_fset thy ty then mk_atom_fset x else
+            if is_rec_type dt then nth fv_frees (body_index dt) $ x else
+            @{term "{} :: atom set"}
       end;
     val arg_nos = 0 upto (length dts - 1)
   in
@@ -315,20 +317,33 @@
   val (_, (_, _, constrs)) = nth descr ith_dtyp;
   val eqs = map2i fv_bn_constr constrs args_in_bns
 in
-  ((bn, fvbn), (fvbn_name, eqs))
+  ((bn, fvbn), eqs)
 end
 *}
 
 ML {*
-fun alpha_bn thy (dt_info : Datatype_Aux.info) alpha_frees ((bn, ith_dtyp, args_in_bns), is_rec) =
+fun fv_bns thy dt_info fv_frees rel_bns =
+let
+  fun mk_fvbn_free (bn, ith, _) =
+    let
+      val fvbn_name = "fv_" ^ (Long_Name.base_name (fst (dest_Const bn)));
+    in
+      (fvbn_name, Free (fvbn_name, fastype_of (nth fv_frees ith)))
+    end;
+  val (fvbn_names, fvbn_frees) = split_list (map mk_fvbn_free rel_bns);
+  val bn_fvbn = (map (fn (bn, _, _) => bn) rel_bns) ~~ fvbn_frees
+  val (l1, l2) = split_list (map (fv_bn thy dt_info fv_frees bn_fvbn) (fvbn_frees ~~ rel_bns));
+in
+  (l1, (fvbn_names ~~ l2))
+end
+*}
+
+
+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)) =
 let
   val {descr, sorts, ...} = dt_info;
   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};
-  val alpha_bn_free = Free(alpha_bn_name, alpha_bn_type);
   val pi = Free("pi", @{typ perm})
   fun alpha_bn_constr (cname, dts) args_in_bn =
   let
@@ -345,12 +360,12 @@
         val argty = fastype_of arg;
         val permute = Const (@{const_name permute}, @{typ perm} --> argty --> argty);
       in
-      if is_rec_type dt then
-        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 (arg, arg2)
+        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
     val arg_nos = 0 upto (length dts - 1)
     val lhss = mk_conjl (map lhs_arg (dts ~~ arg_nos ~~ (args ~~ args2)))
@@ -361,10 +376,33 @@
   val (_, (_, _, constrs)) = nth descr ith_dtyp;
   val eqs = map2i alpha_bn_constr constrs args_in_bns
 in
-  ((bn, alpha_bn_free), (alpha_bn_name, eqs))
+  ((bn, alpha_bn_free), eqs)
 end
 *}
 
+ML {*
+fun alpha_bns thy 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);
+  fun mk_alphabn_free (bn, ith, _) =
+    let
+      val alphabn_name = "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn)));
+      val alphabn_type = nth_dtyp ith --> nth_dtyp ith --> @{typ bool};
+      val alphabn_free = Free(alphabn_name, alphabn_type);
+    in
+      (alphabn_name, alphabn_free)
+    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)
+    (rel_bns ~~ (alphabn_frees ~~ bns_rec)))
+in
+  (alphabn_names, pair)
+end
+*}
+
+
 (* Checks that a list of bindings contains only compatible ones *)
 ML {*
 fun bns_same l =
@@ -384,7 +422,7 @@
   val fv_frees = map Free (fv_names ~~ fv_types);
   val nr_bns = non_rec_binds bindsall;
   val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns;
-  val (bn_fv_bns, fv_bn_names_eqs) = split_list (map (fv_bn thy dt_info fv_frees) rel_bns);
+  val (bn_fv_bns, fv_bn_names_eqs) = fv_bns thy dt_info fv_frees rel_bns;
   val fvbns = map snd bn_fv_bns;
   val (fv_bn_names, fv_bn_eqs) = split_list fv_bn_names_eqs;
   val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
@@ -393,8 +431,8 @@
   val alpha_frees = map Free (alpha_names ~~ alpha_types);
   (* We assume that a bn is either recursive or not *)
   val bns_rec = map (fn (bn, _, _) => not (bn mem nr_bns)) bns;
-  val (bn_alpha_bns, alpha_bn_names_eqs) = split_list (map (alpha_bn thy dt_info alpha_frees) (bns ~~ bns_rec))
-  val (alpha_bn_names, alpha_bn_eqs) = split_list alpha_bn_names_eqs;
+  val (alpha_bn_names, (bn_alpha_bns, alpha_bn_eqs)) =
+    alpha_bns thy 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 =