--- a/Nominal/Fv.thy	Wed Mar 10 11:39:28 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 10 12:53:30 2010 +0100
@@ -321,14 +321,14 @@
         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}
+            (* TODO: if more then check that they are the same and accept *)
           | ([], [(((SOME (bn, _)), _, _), pi)], []) =>
             let
               val alpha_bn = nth alpha_bn_frees (find_index (fn (b, _, _) => b = bn) bns) $ pi $ arg $ arg2