--- a/src/Pure/Syntax/syntax.ML Sat Apr 21 11:07:42 2007 +0200
+++ b/src/Pure/Syntax/syntax.ML Sat Apr 21 11:07:44 2007 +0200
@@ -424,7 +424,7 @@
(* read terms *)
fun read_term get_sort map_const map_free map_type map_sort ctxt is_logtype syn ty str =
- map (TypeExt.decode_types get_sort map_const map_free map_type map_sort)
+ map (TypeExt.decode_term get_sort map_const map_free map_type map_sort)
(read ctxt is_logtype syn ty str);
--- a/src/Pure/Syntax/type_ext.ML Sat Apr 21 11:07:42 2007 +0200
+++ b/src/Pure/Syntax/type_ext.ML Sat Apr 21 11:07:44 2007 +0200
@@ -11,7 +11,7 @@
val sort_of_term: (sort -> sort) -> term -> sort
val term_sorts: (sort -> sort) -> term -> (indexname * sort) list
val typ_of_term: (indexname -> sort) -> (sort -> sort) -> term -> typ
- val decode_types: (((string * int) * sort) list -> string * int -> sort) ->
+ val decode_term: (((string * int) * sort) list -> string * int -> sort) ->
(string -> string option) -> (string -> string option) ->
(typ -> typ) -> (sort -> sort) -> term -> term
val term_of_typ: bool -> typ -> term
@@ -101,9 +101,9 @@
in typ_of t end;
-(* decode_types -- transform parse tree into raw term *)
+(* decode_term -- transform parse tree into raw term *)
-fun decode_types get_sort map_const map_free map_type map_sort tm =
+fun decode_term get_sort map_const map_free map_type map_sort tm =
let
val sort_env = term_sorts map_sort tm;
val decodeT = map_type o typ_of_term (get_sort sort_env) map_sort;