Fixed erroneous type constraint in token_translation function.
authorberghofe
Wed Oct 10 18:39:38 2001 +0200 (2001-10-10)
changeset 11717d808005e6e08
parent 11716 064833efb479
child 11718 92706a69dacc
Fixed erroneous type constraint in token_translation function.
src/Pure/Isar/isar_thy.ML
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Wed Oct 10 18:38:21 2001 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Wed Oct 10 18:39:38 2001 +0200
     1.3 @@ -576,7 +576,7 @@
     1.4      "Theory.add_trfunsT typed_print_translation" o Comment.ignore;
     1.5  
     1.6  val token_translation =
     1.7 -  Context.use_let "val token_translation: (string * string * (string -> string * int)) list"
     1.8 +  Context.use_let "val token_translation: (string * string * (string -> string * real)) list"
     1.9      "Theory.add_tokentrfuns token_translation" o Comment.ignore;
    1.10  
    1.11