Fixed erroneous type constraint in token_translation function.
--- a/src/Pure/Isar/isar_thy.ML Wed Oct 10 18:38:21 2001 +0200
+++ b/src/Pure/Isar/isar_thy.ML Wed Oct 10 18:39:38 2001 +0200
@@ -576,7 +576,7 @@
"Theory.add_trfunsT typed_print_translation" o Comment.ignore;
val token_translation =
- Context.use_let "val token_translation: (string * string * (string -> string * int)) list"
+ Context.use_let "val token_translation: (string * string * (string -> string * real)) list"
"Theory.add_tokentrfuns token_translation" o Comment.ignore;