| changeset 6968 | 7f2977e96a5c |
| parent 6864 | 32b5d68196d2 |
| child 6987 | 4e0defe58b42 |
--- a/src/HOL/Arith.ML Sat Jul 10 21:46:15 1999 +0200 +++ b/src/HOL/Arith.ML Sat Jul 10 21:48:27 1999 +0200 @@ -865,7 +865,7 @@ val not_leD = linorder_not_le RS iffD1; -fun mk_Eq thm = (thm RS Eq_FalseI) handle _ => (thm RS Eq_TrueI); +fun mk_Eq thm = (thm RS Eq_FalseI) handle THM _ => (thm RS Eq_TrueI); val mk_Trueprop = HOLogic.mk_Trueprop;