src/HOL/Tools/record.ML
changeset 33385 fb2358edcfb6
parent 33368 b1cf34f1855c
child 33522 737589bb9bb8
     1.1 --- a/src/HOL/Tools/record.ML	Mon Nov 02 20:34:59 2009 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Mon Nov 02 20:38:46 2009 +0100
     1.3 @@ -262,7 +262,7 @@
     1.4  infixr 0 ==>;
     1.5  
     1.6  val op $$ = Term.list_comb;
     1.7 -val op :== = PrimitiveDefs.mk_defpair;
     1.8 +val op :== = Primitive_Defs.mk_defpair;
     1.9  val op === = Trueprop o HOLogic.mk_eq;
    1.10  val op ==> = Logic.mk_implies;
    1.11