src/Pure/Isar/method.ML
changeset 18921 f47c46d7d654
parent 18877 2ee8333a2ba1
child 18939 18e2a2676d80
--- a/src/Pure/Isar/method.ML	Fri Feb 03 17:08:03 2006 +0100
+++ b/src/Pure/Isar/method.ML	Fri Feb 03 23:12:28 2006 +0100
@@ -325,8 +325,8 @@
     val ps = Logic.strip_assums_hyp g;
     val c = Logic.strip_assums_concl g;
   in
-    if gen_mem (fn ((ps1, c1), (ps2, c2)) =>
-      c1 aconv c2 andalso gen_eq_set op aconv ps1 ps2) ((ps, c), gs) then no_tac
+    if member (fn ((ps1, c1), (ps2, c2)) =>
+      c1 aconv c2 andalso gen_eq_set op aconv ps1 ps2) gs (ps, c) then no_tac
     else (step_tac ctxt THEN_ALL_NEW intprover_tac ctxt ((ps, c) :: gs) (d + 1) lim) i
   end);