src/HOL/Tools/record.ML
changeset 35989 3418cdf1855e
parent 35742 eb8d2f668bfc
child 35994 9cc3df9a606e
     1.1 --- a/src/HOL/Tools/record.ML	Sat Mar 27 17:36:32 2010 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Sat Mar 27 18:07:21 2010 +0100
     1.3 @@ -272,7 +272,7 @@
     1.4  infix 0 :== ===;
     1.5  infixr 0 ==>;
     1.6  
     1.7 -val op :== = Primitive_Defs.mk_defpair;
     1.8 +val op :== = OldGoals.mk_defpair;
     1.9  val op === = Trueprop o HOLogic.mk_eq;
    1.10  val op ==> = Logic.mk_implies;
    1.11