# HG changeset patch
# User wenzelm
# Date 1142939898 -3600
# Node ID 2beb7153e657405a7bddcc1b64024eb8417c7c83
# Parent  73137c0b26f5360459e203ae7747b059fcf9eb1c
moved gen_eq_set to library.ML;

diff -r 73137c0b26f5 -r 2beb7153e657 src/Pure/Isar/method.ML
--- 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);