moved gen_eq_set to library.ML;
authorwenzelm
Tue Mar 21 12:18:18 2006 +0100 (2006-03-21)
changeset 193072beb7153e657
parent 19306 73137c0b26f5
child 19308 033160ed1c8b
moved gen_eq_set to library.ML;
src/Pure/Isar/method.ML
     1.1 --- a/src/Pure/Isar/method.ML	Tue Mar 21 12:18:17 2006 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Tue Mar 21 12:18:18 2006 +0100
     1.3 @@ -297,10 +297,6 @@
     1.4  
     1.5  fun REMDUPS tac = tac THEN_ALL_NEW remdups_tac;
     1.6  
     1.7 -fun gen_eq_set e s1 s2 =
     1.8 -  length s1 = length s2 andalso
     1.9 -  gen_subset e (s1, s2) andalso gen_subset e (s2, s1);
    1.10 -
    1.11  val bires_tac = Tactic.biresolution_from_nets_tac ContextRules.orderlist;
    1.12  
    1.13  fun safe_step_tac ctxt =
    1.14 @@ -324,7 +320,9 @@
    1.15      val c = Logic.strip_assums_concl g;
    1.16    in
    1.17      if member (fn ((ps1, c1), (ps2, c2)) =>
    1.18 -      c1 aconv c2 andalso gen_eq_set op aconv ps1 ps2) gs (ps, c) then no_tac
    1.19 +        c1 aconv c2 andalso
    1.20 +        length ps1 = length ps2 andalso
    1.21 +        gen_eq_set (op aconv) (ps1, ps2)) gs (ps, c) then no_tac
    1.22      else (step_tac ctxt THEN_ALL_NEW intprover_tac ctxt ((ps, c) :: gs) (d + 1) lim) i
    1.23    end);
    1.24