# HG changeset patch
# User wenzelm
# Date 1302089279 -7200
# Node ID 8f798ba04393d344e6a90afb57ea9a4e18f23852
# Parent  29e3967550d5e43a33a5ccbd6589b07fa3103be7
misc tuning and simplification;

diff -r 29e3967550d5 -r 8f798ba04393 src/ZF/Tools/numeral_syntax.ML
--- a/src/ZF/Tools/numeral_syntax.ML	Wed Apr 06 12:58:13 2011 +0200
+++ b/src/ZF/Tools/numeral_syntax.ML	Wed Apr 06 13:27:59 2011 +0200
@@ -1,16 +1,13 @@
 (*  Title:      ZF/Tools/numeral_syntax.ML
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 
-Concrete syntax for generic numerals.  Assumes consts and syntax of
-theory Bin.
+Concrete syntax for generic numerals.
 *)
 
 signature NUMERAL_SYNTAX =
 sig
   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;
 
@@ -73,17 +70,15 @@
 
 (* translation of integer constant tokens to and from binary *)
 
-fun int_tr (*"_Int"*) [t as Free (str, _)] =
+fun int_tr [t as Free (str, _)] =
       Syntax.const @{const_syntax integ_of} $ mk_bin (#value (Syntax.read_xnum str))
-  | int_tr (*"_Int"*) ts = raise TERM ("int_tr", ts);
+  | int_tr ts = raise TERM ("int_tr", ts);
 
-fun int_tr' _ _ (*"integ_of"*) [t] =
-      Syntax.const @{syntax_const "_Int"} $ Syntax.free (show_int t)
-  | int_tr' (_: bool) (_: typ) _ = raise Match;
+fun int_tr' [t] = Syntax.const @{syntax_const "_Int"} $ Syntax.free (show_int t)
+  | int_tr' _ = raise Match;
 
 
 val setup =
- (Sign.add_trfuns ([], [(@{syntax_const "_Int"}, int_tr)], [], []) #>
-  Sign.add_trfunsT [(@{const_syntax integ_of}, int_tr')]);
+ Sign.add_trfuns ([], [(@{syntax_const "_Int"}, int_tr)], [(@{const_syntax integ_of}, int_tr')], []);
 
 end;