--- a/src/Pure/Isar/method.ML Tue Mar 21 12:18:17 2006 +0100
+++ b/src/Pure/Isar/method.ML Tue Mar 21 12:18:18 2006 +0100
@@ -297,10 +297,6 @@
fun REMDUPS tac = tac THEN_ALL_NEW remdups_tac;
-fun gen_eq_set e s1 s2 =
- length s1 = length s2 andalso
- gen_subset e (s1, s2) andalso gen_subset e (s2, s1);
-
val bires_tac = Tactic.biresolution_from_nets_tac ContextRules.orderlist;
fun safe_step_tac ctxt =
@@ -324,7 +320,9 @@
val c = Logic.strip_assums_concl g;
in
if member (fn ((ps1, c1), (ps2, c2)) =>
- c1 aconv c2 andalso gen_eq_set op aconv ps1 ps2) gs (ps, c) then no_tac
+ c1 aconv c2 andalso
+ length ps1 = length ps2 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);