--- a/Nominal/Fv.thy	Wed Mar 17 09:42:56 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 17 09:57:54 2010 +0100
@@ -364,13 +364,16 @@
           val rel_has_binds = filter (fn ((NONE, _, j), _) => j = arg_no
                                        | ((SOME (_, false), _, j), _) => j = arg_no
                                        | _ => false) bind_pis;
+          val rel_has_rec_binds = filter 
+            (fn ((SOME (_, true), _, j), _) => j = arg_no | _ => false) bind_pis;
         in
-          case (rel_in_simp_binds, rel_in_comp_binds, rel_has_binds) of
-            ([], [], []) =>
+          case (rel_in_simp_binds, rel_in_comp_binds, rel_has_binds, rel_has_rec_binds) of
+            ([], [], [], []) =>
               if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2)
               else (HOLogic.mk_eq (arg, arg2))
-          | (_, [], []) => @{term True}
-          | ([], ((((SOME (bn, is_rec)), _, _), pi) :: _), []) =>
+          | (_, [], [], []) => @{term True}
+          | ([], [], [], _) => @{term True}
+          | ([], ((((SOME (bn, is_rec)), _, _), pi) :: _), [], []) =>
             if not (bns_same rel_in_comp_binds) then error "incompatible bindings for an argument" else
             if is_rec then
               let
@@ -409,7 +412,7 @@
               in
                 alpha_bn_const $ arg $ arg2
               end
-          | ([], [], relevant) =>
+          | ([], [], relevant, []) =>
             let
               val (rbinds, rpis) = split_list relevant
               val lhs_binds = fv_binds args rbinds