# HG changeset patch
# User wenzelm
# Date 997285109 -7200
# Node ID 4ff900551340ab0221bb5c03a5ac8e3a18806f5e
# Parent  95071c9e85a335438261395a1b5b4862d24e3701
constify numeral tokens in order to allow translations;

diff -r 95071c9e85a3 -r 4ff900551340 src/HOL/Numeral.thy
--- a/src/HOL/Numeral.thy	Wed Aug 08 17:37:47 2001 +0200
+++ b/src/HOL/Numeral.thy	Wed Aug 08 17:38:29 2001 +0200
@@ -19,8 +19,13 @@
 consts
   number_of :: "bin => 'a::number"
 
+nonterminals
+  numeral
+
 syntax
-  "_Numeral" :: "xnum => 'a"    ("_")
+  "_constify" :: "xnum => numeral"    ("_")
+  "_Numeral" :: "numeral => 'a"    ("_")
+
 
 setup NumeralSyntax.setup
 
diff -r 95071c9e85a3 -r 4ff900551340 src/HOL/Tools/numeral_syntax.ML
--- a/src/HOL/Tools/numeral_syntax.ML	Wed Aug 08 17:37:47 2001 +0200
+++ b/src/HOL/Tools/numeral_syntax.ML	Wed Aug 08 17:38:29 2001 +0200
@@ -56,12 +56,12 @@
 
 (* translation of integer numeral tokens to and from bitstrings *)
 
-fun numeral_tr (*"_Numeral"*) [t as Free (str, _)] =
+fun numeral_tr (*"_Numeral"*) [t as Const (str, _)] =
       (Syntax.const "Numeral.number_of" $ HOLogic.mk_bin (Syntax.read_xnum str))
   | numeral_tr (*"_Numeral"*) ts = raise TERM ("numeral_tr", ts);
 
 fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
-      let val t' = Syntax.const "_Numeral" $ (Syntax.const "_xnum" $ Syntax.free (dest_bin_str t)) in
+      let val t' = Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t) in
         if not (! show_types) andalso can Term.dest_Type T then t'
         else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T
       end