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