--- a/src/ZF/Tools/numeral_syntax.ML Mon Dec 20 15:24:25 2010 +0100
+++ b/src/ZF/Tools/numeral_syntax.ML Mon Dec 20 16:44:33 2010 +0100
@@ -19,12 +19,12 @@
(* bits *)
-fun mk_bit 0 = Syntax.const @{const_syntax "0"}
- | mk_bit 1 = Syntax.const @{const_syntax succ} $ Syntax.const @{const_syntax 0}
+fun mk_bit 0 = Syntax.const @{const_syntax zero}
+ | mk_bit 1 = Syntax.const @{const_syntax succ} $ Syntax.const @{const_syntax zero}
| mk_bit _ = raise Fail "mk_bit";
-fun dest_bit (Const (@{const_syntax "0"}, _)) = 0
- | dest_bit (Const (@{const_syntax succ}, _) $ Const (@{const_syntax "0"}, _)) = 1
+fun dest_bit (Const (@{const_syntax zero}, _)) = 0
+ | dest_bit (Const (@{const_syntax succ}, _) $ Const (@{const_syntax zero}, _)) = 1
| dest_bit _ = raise Match;