# HG changeset patch
# User wenzelm
# Date 1265922397 -3600
# Node ID ff6f60e6ab8580da9961cca01c7d0e29323b4552
# Parent  18cd034922baae15cc4d536e06d36d0812b82709
numeral syntax: clarify parse trees vs. actual terms;
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};

diff -r 18cd034922ba -r ff6f60e6ab85 src/ZF/Bin.thy
--- a/src/ZF/Bin.thy	Thu Feb 11 22:03:37 2010 +0100
+++ b/src/ZF/Bin.thy	Thu Feb 11 22:06:37 2010 +0100
@@ -26,11 +26,6 @@
         | Min
         | Bit ("w: bin", "b: bool")     (infixl "BIT" 90)
 
-use "Tools/numeral_syntax.ML"
-
-syntax
-  "_Int"    :: "xnum => i"        ("_")
-
 consts
   integ_of  :: "i=>i"
   NCons     :: "[i,i]=>i"
@@ -106,6 +101,10 @@
     "bin_mult (v BIT b,w) = cond(b, bin_add(NCons(bin_mult(v,w),0),w),
                                  NCons(bin_mult(v,w),0))"
 
+syntax
+  "_Int"    :: "xnum => i"        ("_")
+
+use "Tools/numeral_syntax.ML"
 setup NumeralSyntax.setup
 
 
diff -r 18cd034922ba -r ff6f60e6ab85 src/ZF/Induct/Multiset.thy
--- a/src/ZF/Induct/Multiset.thy	Thu Feb 11 22:03:37 2010 +0100
+++ b/src/ZF/Induct/Multiset.thy	Thu Feb 11 22:06:37 2010 +0100
@@ -74,9 +74,9 @@
   "a :# M == a \<in> mset_of(M)"
 
 syntax
-  "@MColl" :: "[pttrn, i, o] => i" ("(1{# _ : _./ _#})")
+  "_MColl" :: "[pttrn, i, o] => i" ("(1{# _ : _./ _#})")
 syntax (xsymbols)
-  "@MColl" :: "[pttrn, i, o] => i" ("(1{# _ \<in> _./ _#})")
+  "_MColl" :: "[pttrn, i, o] => i" ("(1{# _ \<in> _./ _#})")
 translations
   "{#x \<in> M. P#}" == "CONST MCollect(M, %x. P)"
 
diff -r 18cd034922ba -r ff6f60e6ab85 src/ZF/List_ZF.thy
--- a/src/ZF/List_ZF.thy	Thu Feb 11 22:03:37 2010 +0100
+++ b/src/ZF/List_ZF.thy	Thu Feb 11 22:06:37 2010 +0100
@@ -16,7 +16,7 @@
 
 syntax
  "[]"        :: i                                       ("[]")
- "@List"     :: "is => i"                                 ("[(_)]")
+ "_List"     :: "is => i"                                 ("[(_)]")
 
 translations
   "[x, xs]"     == "CONST Cons(x, [xs])"
diff -r 18cd034922ba -r ff6f60e6ab85 src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Thu Feb 11 22:03:37 2010 +0100
+++ b/src/ZF/OrdQuant.thy	Thu Feb 11 22:06:37 2010 +0100
@@ -23,9 +23,9 @@
     "OUnion(i,B) == {z: \<Union>x\<in>i. B(x). Ord(i)}"
 
 syntax
-  "@oall"     :: "[idt, i, o] => o"        ("(3ALL _<_./ _)" 10)
-  "@oex"      :: "[idt, i, o] => o"        ("(3EX _<_./ _)" 10)
-  "@OUNION"   :: "[idt, i, i] => i"        ("(3UN _<_./ _)" 10)
+  "_oall"     :: "[idt, i, o] => o"        ("(3ALL _<_./ _)" 10)
+  "_oex"      :: "[idt, i, o] => o"        ("(3EX _<_./ _)" 10)
+  "_OUNION"   :: "[idt, i, i] => i"        ("(3UN _<_./ _)" 10)
 
 translations
   "ALL x<a. P"  == "CONST oall(a, %x. P)"
@@ -33,13 +33,13 @@
   "UN x<a. B"   == "CONST OUnion(a, %x. B)"
 
 syntax (xsymbols)
-  "@oall"     :: "[idt, i, o] => o"        ("(3\<forall>_<_./ _)" 10)
-  "@oex"      :: "[idt, i, o] => o"        ("(3\<exists>_<_./ _)" 10)
-  "@OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
+  "_oall"     :: "[idt, i, o] => o"        ("(3\<forall>_<_./ _)" 10)
+  "_oex"      :: "[idt, i, o] => o"        ("(3\<exists>_<_./ _)" 10)
+  "_OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
 syntax (HTML output)
-  "@oall"     :: "[idt, i, o] => o"        ("(3\<forall>_<_./ _)" 10)
-  "@oex"      :: "[idt, i, o] => o"        ("(3\<exists>_<_./ _)" 10)
-  "@OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
+  "_oall"     :: "[idt, i, o] => o"        ("(3\<forall>_<_./ _)" 10)
+  "_oex"      :: "[idt, i, o] => o"        ("(3\<exists>_<_./ _)" 10)
+  "_OUNION"   :: "[idt, i, i] => i"        ("(3\<Union>_<_./ _)" 10)
 
 
 subsubsection {*simplification of the new quantifiers*}
@@ -203,15 +203,15 @@
     "rex(M, P) == EX x. M(x) & P(x)"
 
 syntax
-  "@rall"     :: "[pttrn, i=>o, o] => o"        ("(3ALL _[_]./ _)" 10)
-  "@rex"      :: "[pttrn, i=>o, o] => o"        ("(3EX _[_]./ _)" 10)
+  "_rall"     :: "[pttrn, i=>o, o] => o"        ("(3ALL _[_]./ _)" 10)
+  "_rex"      :: "[pttrn, i=>o, o] => o"        ("(3EX _[_]./ _)" 10)
 
 syntax (xsymbols)
-  "@rall"     :: "[pttrn, i=>o, o] => o"        ("(3\<forall>_[_]./ _)" 10)
-  "@rex"      :: "[pttrn, i=>o, o] => o"        ("(3\<exists>_[_]./ _)" 10)
+  "_rall"     :: "[pttrn, i=>o, o] => o"        ("(3\<forall>_[_]./ _)" 10)
+  "_rex"      :: "[pttrn, i=>o, o] => o"        ("(3\<exists>_[_]./ _)" 10)
 syntax (HTML output)
-  "@rall"     :: "[pttrn, i=>o, o] => o"        ("(3\<forall>_[_]./ _)" 10)
-  "@rex"      :: "[pttrn, i=>o, o] => o"        ("(3\<exists>_[_]./ _)" 10)
+  "_rall"     :: "[pttrn, i=>o, o] => o"        ("(3\<forall>_[_]./ _)" 10)
+  "_rex"      :: "[pttrn, i=>o, o] => o"        ("(3\<exists>_[_]./ _)" 10)
 
 translations
   "ALL x[M]. P"  == "CONST rall(M, %x. P)"
diff -r 18cd034922ba -r ff6f60e6ab85 src/ZF/Tools/numeral_syntax.ML
--- a/src/ZF/Tools/numeral_syntax.ML	Thu Feb 11 22:03:37 2010 +0100
+++ b/src/ZF/Tools/numeral_syntax.ML	Thu Feb 11 22:06:37 2010 +0100
@@ -7,92 +7,83 @@
 
 signature NUMERAL_SYNTAX =
 sig
-  val dest_bin : term -> int
-  val mk_bin   : int -> term
-  val int_tr   : term list -> term
-  val int_tr'  : bool -> typ -> term list -> term
-  val setup    : theory -> theory
+  val make_binary: int -> int list
+  val dest_binary: int list -> int
+  val int_tr: term list -> term
+  val int_tr': bool -> typ -> term list -> term
+  val setup: theory -> theory
 end;
 
 structure NumeralSyntax: NUMERAL_SYNTAX =
 struct
 
-(* Bits *)
+(* bits *)
 
-fun mk_bit 0 = @{term "0"}
-  | mk_bit 1 = @{term "succ(0)"}
+fun mk_bit 0 = Syntax.const @{const_syntax "0"}
+  | mk_bit 1 = Syntax.const @{const_syntax succ} $ Syntax.const @{const_syntax 0}
   | mk_bit _ = sys_error "mk_bit";
 
-fun dest_bit (Const (@{const_name "0"}, _)) = 0
-  | dest_bit (Const (@{const_name succ}, _) $ Const (@{const_name "0"}, _)) = 1
+fun dest_bit (Const (@{const_syntax "0"}, _)) = 0
+  | dest_bit (Const (@{const_syntax succ}, _) $ Const (@{const_syntax "0"}, _)) = 1
   | dest_bit _ = raise Match;
 
 
-(* Bit strings *)   (*we try to handle superfluous leading digits nicely*)
+(* bit strings *)
+
+fun make_binary 0 = []
+  | make_binary ~1 = [~1]
+  | make_binary n = (n mod 2) :: make_binary (n div 2);
 
+fun dest_binary [] = 0
+  | dest_binary (b :: bs) = b + 2 * dest_binary bs;
+
+
+(*try to handle superfluous leading digits nicely*)
 fun prefix_len _ [] = 0
   | prefix_len pred (x :: xs) =
       if pred x then 1 + prefix_len pred xs else 0;
 
 fun mk_bin i =
-  let fun bin_of_int 0  = []
-        | bin_of_int ~1 = [~1]
-        | bin_of_int n  = (n mod 2) :: bin_of_int (n div 2);
-
-      fun term_of [] = @{const Pls}
-            | term_of [~1] = @{const Min}
-            | term_of (b :: bs) = @{const Bit} $ term_of bs $ mk_bit b;
-  in
-    term_of (bin_of_int i)
-  end;
+  let
+    fun term_of [] = Syntax.const @{const_syntax Pls}
+      | term_of [~1] = Syntax.const @{const_syntax Min}
+      | term_of (b :: bs) = Syntax.const @{const_syntax Bit} $ term_of bs $ mk_bit b;
+  in term_of (make_binary i) end;
 
-(*we consider all "spellings", since they could vary depending on the caller*)
-fun bin_of (Const ("Pls", _)) = []
-  | bin_of (Const ("bin.Pls", _)) = []
-  | bin_of (Const ("Bin.bin.Pls", _)) = []
-  | bin_of (Const ("Min", _)) = [~1]
-  | bin_of (Const ("bin.Min", _)) = [~1]
-  | bin_of (Const ("Bin.bin.Min", _)) = [~1]
-  | bin_of (Const ("Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
-  | bin_of (Const ("bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
-  | bin_of (Const ("Bin.bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
+fun bin_of (Const (@{const_syntax Pls}, _)) = []
+  | bin_of (Const (@{const_syntax Min}, _)) = [~1]
+  | bin_of (Const (@{const_syntax Bit}, _) $ bs $ b) = dest_bit b :: bin_of bs
   | bin_of _ = raise Match;
 
-(*Convert a list of bits to an integer*)
-fun integ_of [] = 0
-  | integ_of (b :: bs) = b + 2 * integ_of bs;
-
-val dest_bin = integ_of o bin_of;
-
-(*leading 0s and (for negative numbers) -1s cause complications, though they 
+(*Leading 0s and (for negative numbers) -1s cause complications, though they 
   should never arise in normal use. The formalization used in HOL prevents 
   them altogether.*)
 fun show_int t =
   let
     val rev_digs = bin_of t;
     val (sign, zs) =
-        (case rev rev_digs of
-             ~1 :: bs => ("-", prefix_len (equal 1) bs)
-           | bs =>       ("",  prefix_len (equal 0) bs));
-    val num = string_of_int (abs (integ_of rev_digs));
+      (case rev rev_digs of
+         ~1 :: bs => ("-", prefix_len (equal 1) bs)
+      | bs => ("",  prefix_len (equal 0) bs));
+    val num = string_of_int (abs (dest_binary rev_digs));
   in
     "#" ^ sign ^ implode (replicate zs "0") ^ num
   end;
 
 
-
 (* translation of integer constant tokens to and from binary *)
 
 fun int_tr (*"_Int"*) [t as Free (str, _)] =
-      Syntax.const "integ_of" $ mk_bin (#value (Syntax.read_xnum str))
+      Syntax.const @{const_syntax integ_of} $ mk_bin (#value (Syntax.read_xnum str))
   | int_tr (*"_Int"*) ts = raise TERM ("int_tr", ts);
 
-fun int_tr' _ _ (*"integ_of"*) [t] = Syntax.const "_Int" $ Syntax.free (show_int t)
-  | int_tr' (_:bool) (_:typ)     _ = raise Match;
+fun int_tr' _ _ (*"integ_of"*) [t] =
+      Syntax.const @{syntax_const "_Int"} $ Syntax.free (show_int t)
+  | int_tr' (_: bool) (_: typ) _ = raise Match;
 
 
 val setup =
- (Sign.add_trfuns ([], [("_Int", int_tr)], [], []) #>
-  Sign.add_trfunsT [("integ_of", int_tr'), ("Bin.integ_of", int_tr')]);
+ (Sign.add_trfuns ([], [(@{syntax_const "_Int"}, int_tr)], [], []) #>
+  Sign.add_trfunsT [(@{const_syntax integ_of}, int_tr')]);
 
 end;
diff -r 18cd034922ba -r ff6f60e6ab85 src/ZF/UNITY/Union.thy
--- a/src/ZF/UNITY/Union.thy	Thu Feb 11 22:03:37 2010 +0100
+++ b/src/ZF/UNITY/Union.thy	Thu Feb 11 22:06:37 2010 +0100
@@ -41,8 +41,8 @@
       SKIP \<in> X & (\<forall>G \<in> program. Acts(G) \<subseteq> (\<Union>F \<in> X. Acts(F)) --> G \<in> X)"
   
 syntax
-  "@JOIN1"     :: "[pttrns, i] => i"         ("(3JN _./ _)" 10)
-  "@JOIN"      :: "[pttrn, i, i] => i"       ("(3JN _:_./ _)" 10)
+  "_JOIN1"     :: "[pttrns, i] => i"         ("(3JN _./ _)" 10)
+  "_JOIN"      :: "[pttrn, i, i] => i"       ("(3JN _:_./ _)" 10)
 
 translations
   "JN x:A. B"   == "CONST JOIN(A, (%x. B))"
@@ -54,8 +54,8 @@
   Join  (infixl "\<squnion>" 65)
 
 syntax (xsymbols)
-  "@JOIN1"  :: "[pttrns, i] => i"     ("(3\<Squnion> _./ _)" 10)
-  "@JOIN"   :: "[pttrn, i, i] => i"   ("(3\<Squnion> _ \<in> _./ _)" 10)
+  "_JOIN1"  :: "[pttrns, i] => i"     ("(3\<Squnion> _./ _)" 10)
+  "_JOIN"   :: "[pttrn, i, i] => i"   ("(3\<Squnion> _ \<in> _./ _)" 10)
 
 
 subsection{*SKIP*}
diff -r 18cd034922ba -r ff6f60e6ab85 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Thu Feb 11 22:03:37 2010 +0100
+++ b/src/ZF/ZF.thy	Thu Feb 11 22:06:37 2010 +0100
@@ -105,26 +105,26 @@
 
 syntax
   ""          :: "i => is"                   ("_")
-  "@Enum"     :: "[i, is] => is"             ("_,/ _")
+  "_Enum"     :: "[i, is] => is"             ("_,/ _")
 
-  "@Finset"   :: "is => i"                   ("{(_)}")
-  "@Tuple"    :: "[i, is] => i"              ("<(_,/ _)>")
-  "@Collect"  :: "[pttrn, i, o] => i"        ("(1{_: _ ./ _})")
-  "@Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})")
-  "@RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _: _})" [51,0,51])
-  "@INTER"    :: "[pttrn, i, i] => i"        ("(3INT _:_./ _)" 10)
-  "@UNION"    :: "[pttrn, i, i] => i"        ("(3UN _:_./ _)" 10)
-  "@PROD"     :: "[pttrn, i, i] => i"        ("(3PROD _:_./ _)" 10)
-  "@SUM"      :: "[pttrn, i, i] => i"        ("(3SUM _:_./ _)" 10)
-  "@lam"      :: "[pttrn, i, i] => i"        ("(3lam _:_./ _)" 10)
-  "@Ball"     :: "[pttrn, i, o] => o"        ("(3ALL _:_./ _)" 10)
-  "@Bex"      :: "[pttrn, i, o] => o"        ("(3EX _:_./ _)" 10)
+  "_Finset"   :: "is => i"                   ("{(_)}")
+  "_Tuple"    :: "[i, is] => i"              ("<(_,/ _)>")
+  "_Collect"  :: "[pttrn, i, o] => i"        ("(1{_: _ ./ _})")
+  "_Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})")
+  "_RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _: _})" [51,0,51])
+  "_INTER"    :: "[pttrn, i, i] => i"        ("(3INT _:_./ _)" 10)
+  "_UNION"    :: "[pttrn, i, i] => i"        ("(3UN _:_./ _)" 10)
+  "_PROD"     :: "[pttrn, i, i] => i"        ("(3PROD _:_./ _)" 10)
+  "_SUM"      :: "[pttrn, i, i] => i"        ("(3SUM _:_./ _)" 10)
+  "_lam"      :: "[pttrn, i, i] => i"        ("(3lam _:_./ _)" 10)
+  "_Ball"     :: "[pttrn, i, o] => o"        ("(3ALL _:_./ _)" 10)
+  "_Bex"      :: "[pttrn, i, o] => o"        ("(3EX _:_./ _)" 10)
 
   (** Patterns -- extends pre-defined type "pttrn" used in abstractions **)
 
-  "@pattern"  :: "patterns => pttrn"         ("<_>")
+  "_pattern"  :: "patterns => pttrn"         ("<_>")
   ""          :: "pttrn => patterns"         ("_")
-  "@patterns" :: "[pttrn, patterns] => patterns"  ("_,/_")
+  "_patterns" :: "[pttrn, patterns] => patterns"  ("_,/_")
 
 translations
   "{x, xs}"     == "CONST cons(x, {xs})"
@@ -158,18 +158,18 @@
   Inter           ("\<Inter>_" [90] 90)
 
 syntax (xsymbols)
-  "@Collect"  :: "[pttrn, i, o] => i"        ("(1{_ \<in> _ ./ _})")
-  "@Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
-  "@RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _ \<in> _})" [51,0,51])
-  "@UNION"    :: "[pttrn, i, i] => i"        ("(3\<Union>_\<in>_./ _)" 10)
-  "@INTER"    :: "[pttrn, i, i] => i"        ("(3\<Inter>_\<in>_./ _)" 10)
-  "@PROD"     :: "[pttrn, i, i] => i"        ("(3\<Pi>_\<in>_./ _)" 10)
-  "@SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sigma>_\<in>_./ _)" 10)
-  "@lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
-  "@Ball"     :: "[pttrn, i, o] => o"        ("(3\<forall>_\<in>_./ _)" 10)
-  "@Bex"      :: "[pttrn, i, o] => o"        ("(3\<exists>_\<in>_./ _)" 10)
-  "@Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")
-  "@pattern"  :: "patterns => pttrn"         ("\<langle>_\<rangle>")
+  "_Collect"  :: "[pttrn, i, o] => i"        ("(1{_ \<in> _ ./ _})")
+  "_Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
+  "_RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _ \<in> _})" [51,0,51])
+  "_UNION"    :: "[pttrn, i, i] => i"        ("(3\<Union>_\<in>_./ _)" 10)
+  "_INTER"    :: "[pttrn, i, i] => i"        ("(3\<Inter>_\<in>_./ _)" 10)
+  "_PROD"     :: "[pttrn, i, i] => i"        ("(3\<Pi>_\<in>_./ _)" 10)
+  "_SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sigma>_\<in>_./ _)" 10)
+  "_lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
+  "_Ball"     :: "[pttrn, i, o] => o"        ("(3\<forall>_\<in>_./ _)" 10)
+  "_Bex"      :: "[pttrn, i, o] => o"        ("(3\<exists>_\<in>_./ _)" 10)
+  "_Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")
+  "_pattern"  :: "patterns => pttrn"         ("\<langle>_\<rangle>")
 
 notation (HTML output)
   cart_prod       (infixr "\<times>" 80) and
@@ -182,18 +182,18 @@
   Inter           ("\<Inter>_" [90] 90)
 
 syntax (HTML output)
-  "@Collect"  :: "[pttrn, i, o] => i"        ("(1{_ \<in> _ ./ _})")
-  "@Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
-  "@RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _ \<in> _})" [51,0,51])
-  "@UNION"    :: "[pttrn, i, i] => i"        ("(3\<Union>_\<in>_./ _)" 10)
-  "@INTER"    :: "[pttrn, i, i] => i"        ("(3\<Inter>_\<in>_./ _)" 10)
-  "@PROD"     :: "[pttrn, i, i] => i"        ("(3\<Pi>_\<in>_./ _)" 10)
-  "@SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sigma>_\<in>_./ _)" 10)
-  "@lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
-  "@Ball"     :: "[pttrn, i, o] => o"        ("(3\<forall>_\<in>_./ _)" 10)
-  "@Bex"      :: "[pttrn, i, o] => o"        ("(3\<exists>_\<in>_./ _)" 10)
-  "@Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")
-  "@pattern"  :: "patterns => pttrn"         ("\<langle>_\<rangle>")
+  "_Collect"  :: "[pttrn, i, o] => i"        ("(1{_ \<in> _ ./ _})")
+  "_Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _ \<in> _, _})")
+  "_RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _ \<in> _})" [51,0,51])
+  "_UNION"    :: "[pttrn, i, i] => i"        ("(3\<Union>_\<in>_./ _)" 10)
+  "_INTER"    :: "[pttrn, i, i] => i"        ("(3\<Inter>_\<in>_./ _)" 10)
+  "_PROD"     :: "[pttrn, i, i] => i"        ("(3\<Pi>_\<in>_./ _)" 10)
+  "_SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sigma>_\<in>_./ _)" 10)
+  "_lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
+  "_Ball"     :: "[pttrn, i, o] => o"        ("(3\<forall>_\<in>_./ _)" 10)
+  "_Bex"      :: "[pttrn, i, o] => o"        ("(3\<exists>_\<in>_./ _)" 10)
+  "_Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")
+  "_pattern"  :: "patterns => pttrn"         ("\<langle>_\<rangle>")
 
 
 finalconsts
diff -r 18cd034922ba -r ff6f60e6ab85 src/ZF/int_arith.ML
--- a/src/ZF/int_arith.ML	Thu Feb 11 22:03:37 2010 +0100
+++ b/src/ZF/int_arith.ML	Thu Feb 11 22:06:37 2010 +0100
@@ -7,15 +7,40 @@
 structure Int_Numeral_Simprocs =
 struct
 
+(* abstract syntax operations *)
+
+fun mk_bit 0 = @{term "0"}
+  | mk_bit 1 = @{term "succ(0)"}
+  | mk_bit _ = sys_error "mk_bit";
+
+fun dest_bit @{term "0"} = 0
+  | dest_bit @{term "succ(0)"} = 1
+  | dest_bit _ = raise Match;
+
+fun mk_bin i =
+  let
+    fun term_of [] = @{term Pls}
+      | term_of [~1] = @{term Min}
+      | term_of (b :: bs) = @{term Bit} $ term_of bs $ mk_bit b;
+  in term_of (NumeralSyntax.make_binary i) end;
+
+fun dest_bin tm =
+  let
+    fun bin_of @{term Pls} = []
+      | bin_of @{term Min} = [~1]
+      | bin_of (@{term Bit} $ bs $ b) = dest_bit b :: bin_of bs
+      | bin_of _ = sys_error "dest_bin";
+  in NumeralSyntax.dest_binary (bin_of tm) end;
+
+
 (*Utilities*)
 
-fun mk_numeral n = @{const integ_of} $ NumeralSyntax.mk_bin n;
+fun mk_numeral i = @{const integ_of} $ mk_bin i;
 
 (*Decodes a binary INTEGER*)
 fun dest_numeral (Const(@{const_name integ_of}, _) $ w) =
-     (NumeralSyntax.dest_bin w
-      handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
-  | dest_numeral t =  raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
+     (dest_bin w handle SYS_ERROR _ => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
+  | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
 
 fun find_first_numeral past (t::terms) =
         ((dest_numeral t, rev past @ terms)