diff -r 4a10338c2535 -r 56ce001cdb87 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Wed Mar 10 16:50:42 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 10 16:51:15 2010 +0100
@@ -238,6 +238,12 @@
 end
 *}
 
+(* Checks that a list of bindings contains only compatible ones *)
+ML {*
+fun bns_same l =
+  length (distinct (op =) (map (fn ((b, _, _), _) => b) l)) = 1
+*}
+
 ML {* fn x => split_list(flat x) *}
 ML {* fn x => apsnd flat (split_list (map split_list x)) *}
 (* TODO: Notice datatypes without bindings and replace alpha with equality *)
@@ -321,21 +327,22 @@
         let
           val rel_in_simp_binds = filter (fn ((NONE, i, _), _) => i = arg_no | _ => false) bind_pis;
           val rel_in_comp_binds = filter (fn ((SOME _, i, _), _) => i = arg_no | _ => false) bind_pis;
-          val rel_has_binds = filter (fn ((SOME _, _, j), _) => j = arg_no | _ => false) bind_pis;
+          val rel_has_binds = filter (fn ((_, _, j), _) => j = arg_no | _ => false) bind_pis;
         in
           case (rel_in_simp_binds, rel_in_comp_binds, rel_has_binds) of
             ([], [], []) =>
               if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2)
               else (HOLogic.mk_eq (arg, arg2))
-            (* TODO: if more then check and accept *)
           | (_, [], []) => @{term True}
-          | ([], [(((SOME (bn, _)), _, _), pi)], []) =>
+          | ([], ((((SOME (bn, _)), _, _), pi) :: _), []) =>
             let
               val alpha_bn = nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns) $ pi $ arg $ arg2
               val ty = fastype_of (bn $ arg)
               val permute = Const(@{const_name permute}, @{typ perm} --> ty --> ty)
             in
-              HOLogic.mk_conj (alpha_bn, HOLogic.mk_eq (permute $ pi $ (bn $ arg), (bn $ arg2)))
+              if bns_same rel_in_comp_binds then
+                HOLogic.mk_conj (alpha_bn, HOLogic.mk_eq (permute $ pi $ (bn $ arg), (bn $ arg2)))
+              else error "incompatible bindings for one argument"
             end
           | ([], [], relevant) =>
             let