src/Tools/intuitionistic.ML

--- a/src/Tools/intuitionistic.ML	Tue Oct 20 16:13:01 2009 +0200
+++ b/src/Tools/intuitionistic.ML	Wed Oct 21 08:14:38 2009 +0200
@@ -50,7 +50,7 @@
     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);