diff -r 5180e11e4e42 -r d86dbde1000c src/HOL/Tools/record_package.ML
--- 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;