| changeset 24255 | d86dbde1000c |
| parent 24219 | e558fe311376 |
| child 24624 | b8383b1bbae3 |
--- a/src/HOL/Tools/record_package.ML Tue Aug 14 00:52:59 2007 +0200 +++ b/src/HOL/Tools/record_package.ML Tue Aug 14 13:20:12 2007 +0200 @@ -137,7 +137,7 @@ infixr 0 ==>; val (op $$) = Term.list_comb; -val (op :==) = Logic.mk_defpair; +val (op :==) = PrimitiveDefs.mk_defpair; val (op ===) = Trueprop o HOLogic.mk_eq; val (op ==>) = Logic.mk_implies;