--- 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);