src/Tools/intuitionistic.ML

     val c = Logic.strip_assums_concl g;
   in
     if member (fn ((ps1, c1), (ps2, c2)) =>
         c1 aconv c2 andalso
         length ps1 = length ps2 andalso
-        gen_eq_set (op aconv) (ps1, ps2)) gs (ps, c) then no_tac
+        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);
 
 in