# HG changeset patch
# User nipkow
# Date 808741682 -7200
# Node ID 87e29e18e97066764abcf21730b565d39c21e9f6
# Parent  f191f25a5ec86e7587592cc809cf2aa4233dbc94
fixed bug in findI
removed duplicates in findEs

diff -r f191f25a5ec8 -r 87e29e18e970 src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Thu Aug 17 15:07:09 1995 +0200
+++ b/src/Pure/Thy/thm_database.ML	Fri Aug 18 12:28:02 1995 +0200
@@ -148,7 +148,7 @@
             let val {prop,sign,...} = rep_thm thm
             in select(named_thms,
                       if Sign.subsig(sign,signobj) andalso
-                         matches(prop,#tsig(Sign.rep_sg sign))
+                         matches(prop,#tsig(Sign.rep_sg signobj))
                       then p::sels else sels)
             end
         | select([],sels) = sels
@@ -171,8 +171,10 @@
 fun findI i = find_intros(concl_of_goal i,#sign(rep_thm(topthm())));
 
 fun findEs i =
-  let val sign = #sign(rep_thm(topthm()))
-  in flat(map (find_elims sign) (prems_of_goal i)) end;
+  let fun eq_nth((n1,th1),(n2,th2)) = n1=n2 andalso eq_thm(th1,th2);
+      val sign = #sign(rep_thm(topthm()))
+      val thmss = map (find_elims sign) (prems_of_goal i)
+  in foldl (gen_union eq_nth) ([],thmss) end;
 
 fun findE i j =
   let val sign = #sign(rep_thm(topthm()))