changeset 22360 | 26ead7ed4f4b |
parent 22320 | d5260836d662 |
child 22395 | b573f1f566e1 |
--- a/src/HOL/Library/EfficientNat.thy Mon Feb 26 21:34:16 2007 +0100 +++ b/src/HOL/Library/EfficientNat.thy Mon Feb 26 23:18:24 2007 +0100 @@ -261,7 +261,7 @@ [] => NONE | thps => let val (ths1, ths2) = split_list thps - in SOME (subtract eq_thm (th :: ths1) thms @ ths2) end + in SOME (subtract Thm.eq_thm (th :: ths1) thms @ ths2) end end in case get_first mk_thms eqs of