src/Pure/tactic.ML
changeset 22360 26ead7ed4f4b
parent 21708 45e7491bea47
child 22560 f19ddf96c323
     1.1 --- a/src/Pure/tactic.ML	Mon Feb 26 21:34:16 2007 +0100
     1.2 +++ b/src/Pure/tactic.ML	Mon Feb 26 23:18:24 2007 +0100
     1.3 @@ -421,7 +421,7 @@
     1.4      foldr insert_tagged_brl netpair (taglist 1 brls);
     1.5  
     1.6  (*delete one kbrl from the pair of nets*)
     1.7 -fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Drule.eq_thm_prop (th, th')
     1.8 +fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th')
     1.9  
    1.10  fun delete_tagged_brl (brl as (eres, th), (inet, enet)) =
    1.11    (if eres then