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