# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268222024 -3600
# Node ID e81857969443ef683381164aa80037882be058f7
# Parent  3dd4d4376f96f09b14c7b9c155af5f69b4fb9955# Parent  4eaae533efc39050c18be45f7390b4d9575034c3
merge

diff -r 4eaae533efc3 -r e81857969443 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Wed Mar 10 12:48:55 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 10 12:53:44 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