src/HOL/Integ/presburger.ML

    ("Numeral.Bit", iT --> bitT --> iT),
    ("Numeral.Pls", iT),
    ("Numeral.Min", iT),
    ("Numeral.number_of", iT --> iT),
    ("Numeral.number_of", iT --> nT),
-   ("0", nT),
-   ("0", iT),
-   ("1", nT),
-   ("1", iT),
+   ("HOL.zero", nT),
+   ("HOL.zero", iT),
+   ("HOL.one", nT),
+   ("HOL.one", iT),
    ("False", bT),
    ("True", bT)];
 
 (* Preparation of the formula to be sent to the Integer quantifier *)
 (* elimination procedure                                           *)