1.1 --- a/src/Pure/Isar/method.ML Fri Feb 03 17:08:03 2006 +0100
1.2 +++ b/src/Pure/Isar/method.ML Fri Feb 03 23:12:28 2006 +0100
1.3 @@ -325,8 +325,8 @@
1.4 val ps = Logic.strip_assums_hyp g;
1.5 val c = Logic.strip_assums_concl g;
1.6 in
1.7 - if gen_mem (fn ((ps1, c1), (ps2, c2)) =>
1.8 - c1 aconv c2 andalso gen_eq_set op aconv ps1 ps2) ((ps, c), gs) then no_tac
1.9 + if member (fn ((ps1, c1), (ps2, c2)) =>
1.10 + c1 aconv c2 andalso gen_eq_set op aconv ps1 ps2) gs (ps, c) then no_tac
1.11 else (step_tac ctxt THEN_ALL_NEW intprover_tac ctxt ((ps, c) :: gs) (d + 1) lim) i
1.12 end);
1.13