src/Pure/Isar/context_rules.ML
changeset 13105 3d1e7a199bdc
parent 12805 3be853cf19cf
child 13372 18790d503fe0
     1.1 --- a/src/Pure/Isar/context_rules.ML	Tue May 07 14:24:30 2002 +0200
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Tue May 07 14:26:32 2002 +0200
     1.3 @@ -103,7 +103,7 @@
     1.4  
     1.5  fun del_rule th (rs as Rules {next, rules, netpairs, wrappers}) =
     1.6    let
     1.7 -    fun eq_th (_, (_, th')) = Thm.eq_thm (th, th');
     1.8 +    fun eq_th (_, (_, th')) = Drule.eq_thm_prop (th, th');
     1.9      fun del b netpair = delete_tagged_brl ((b, th), netpair) handle Net.DELETE => netpair;
    1.10    in
    1.11      if not (exists eq_th rules) then rs
    1.12 @@ -135,7 +135,7 @@
    1.13      let
    1.14        val wrappers = (gen_merge_lists' eq_snd ws1 ws2, gen_merge_lists' eq_snd ws1' ws2');
    1.15        val rules = gen_merge_lists' (fn ((_, (k1, th1)), (_, (k2, th2))) =>
    1.16 -          k1 = k2 andalso Thm.eq_thm (th1, th2)) rules1 rules2;
    1.17 +          k1 = k2 andalso Drule.eq_thm_prop (th1, th2)) rules1 rules2;
    1.18        val next = ~ (length rules);
    1.19        val netpairs = foldl (fn (nps, (n, (w, ((i, b), th)))) =>
    1.20            map_nth_elem i (curry insert_tagged_brl ((w, n), (b, th))) nps)