# HG changeset patch # User berghofe # Date 1002731978 -7200 # Node ID d808005e6e085fb7c977c0cc3a7d3ad0bde2f76b # Parent 064833efb4797d8f747b80e57b14ccb91768f4f9 Fixed erroneous type constraint in token_translation function. diff -r 064833efb479 -r d808005e6e08 src/Pure/Isar/isar_thy.ML --- 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;