src/Pure/tactic.ML
changeset 13105 3d1e7a199bdc
parent 12847 afa356dbcb15
child 13559 51c3ac47d127
     1.1 --- a/src/Pure/tactic.ML	Tue May 07 14:24:30 2002 +0200
     1.2 +++ b/src/Pure/tactic.ML	Tue May 07 14:26:32 2002 +0200
     1.3 @@ -410,7 +410,7 @@
     1.4  
     1.5  (*delete one kbrl from the pair of nets*)
     1.6  local
     1.7 -  fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = eq_thm (th, th')
     1.8 +  fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Drule.eq_thm_prop (th, th')
     1.9  in
    1.10  fun delete_tagged_brl (brl as (eres, th), (inet, enet)) =
    1.11    if eres then