# HG changeset patch
# User wenzelm
# Date 1177146464 -7200
# Node ID ccbd31bc1ef7d7f5579d126dfc4648079fece69b
# Parent  5c1752279f25883b2a74b1668e29edb18f9b94e4
TypeExt.decode_term;

diff -r 5c1752279f25 -r ccbd31bc1ef7 src/Pure/Syntax/syntax.ML
--- 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);
 
 
diff -r 5c1752279f25 -r ccbd31bc1ef7 src/Pure/Syntax/type_ext.ML
--- 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;