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