# HG changeset patch
# User wenzelm
# Date 920977569 -3600
# Node ID 15652e058e28b8db28ee0c9693c522d5528c43fd
# Parent  353a8a9d9d2c6d1dba28a6d8aaddb97e351aab57
token translation: real;

diff -r 353a8a9d9d2c -r 15652e058e28 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Mar 09 12:05:07 1999 +0100
+++ b/src/Pure/sign.ML	Tue Mar 09 12:06:09 1999 +0100
@@ -114,7 +114,7 @@
   val add_trfunsT:
     (string * (bool -> typ -> term list -> term)) list -> sg -> sg
   val add_tokentrfuns:
-    (string * string * (string -> string * int)) list -> sg -> sg
+    (string * string * (string -> string * real)) list -> sg -> sg
   val add_trrules: (xstring * string) Syntax.trrule list -> sg -> sg
   val add_trrules_i: ast Syntax.trrule list -> sg -> sg
   val add_path: string -> sg -> sg
diff -r 353a8a9d9d2c -r 15652e058e28 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Tue Mar 09 12:05:07 1999 +0100
+++ b/src/Pure/theory.ML	Tue Mar 09 12:06:09 1999 +0100
@@ -24,8 +24,8 @@
   val subthy: theory * theory -> bool
   val eq_thy: theory * theory -> bool
   val cert_axm: Sign.sg -> string * term -> string * term
-  val read_def_axm: Sign.sg * (indexname -> typ option) * (indexname -> sort option) -> string list ->
-    string * string -> string * term
+  val read_def_axm: Sign.sg * (indexname -> typ option) * (indexname -> sort option) ->
+    string list -> string * string -> string * term
   val read_axm: Sign.sg -> string * string -> string * term
   val inferT_axm: Sign.sg -> string * term -> string * term
   val merge_theories: string -> theory * theory -> theory
@@ -65,7 +65,9 @@
   val add_trfunsT:
     (string * (bool -> typ -> term list -> term)) list -> theory -> theory
   val add_tokentrfuns:
-    (string * string * (string -> string * int)) list -> theory -> theory
+    (string * string * (string -> string * real)) list -> theory -> theory
+  val add_mode_tokentrfuns: string -> (string * (string -> string * real)) list
+    -> theory -> theory
   val add_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
   val add_trrules_i: Syntax.ast Syntax.trrule list -> theory -> theory
   val add_axioms: (bstring * string) list -> theory -> theory
@@ -196,6 +198,7 @@
 val add_trfuns       = ext_sign Sign.add_trfuns;
 val add_trfunsT      = ext_sign Sign.add_trfunsT;
 val add_tokentrfuns  = ext_sign Sign.add_tokentrfuns;
+fun add_mode_tokentrfuns m = add_tokentrfuns o map (fn (s, f) => (m, s, f));
 val add_trrules      = ext_sign Sign.add_trrules;
 val add_trrules_i    = ext_sign Sign.add_trrules_i;
 val add_path         = ext_sign Sign.add_path;
@@ -207,6 +210,7 @@
 val copy             = prep_ext;	(*an approximation ...*)
 
 
+
 (** add axioms **)
 
 (* prepare axioms *)