diff -r 08294f4d6c08 -r 6e2dfe52b271 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Wed Mar 10 13:10:00 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 10 13:29:12 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 *)
@@ -328,14 +334,15 @@
               if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2)
               else (HOLogic.mk_eq (arg, arg2))
           | (_, [], []) => @{term True}
-            (* TODO: if more then check that they are the same and accept *)
-          | ([], [(((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