diff -r edeb1bbcd479 -r 79138d75405f src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Wed Nov 28 23:29:48 2001 +0100
+++ b/src/Pure/Syntax/syntax.ML	Wed Nov 28 23:30:24 2001 +0100
@@ -50,9 +50,9 @@
   val print_syntax: syntax -> unit
   val test_read: syntax -> string -> string -> unit
   val read: syntax -> typ -> string -> term list
-  val read_typ: syntax -> ((indexname * sort) list -> indexname -> sort) -> string -> typ
+  val read_typ: syntax -> ((indexname * sort) list -> indexname -> sort) -> (sort -> sort) ->
+    string -> typ
   val read_sort: syntax -> string -> sort
-  val simple_read_typ: string -> typ
   val pretty_term: syntax -> bool -> term -> Pretty.T
   val pretty_typ: syntax -> typ -> Pretty.T
   val pretty_sort: syntax -> sort -> Pretty.T
@@ -371,16 +371,11 @@
 
 (* read types *)
 
-fun read_typ syn get_sort str =
+fun read_typ syn get_sort map_sort str =
   (case read syn SynExt.typeT str of
-    [t] => TypeExt.typ_of_term (get_sort (TypeExt.raw_term_sorts t)) t
+    [t] => TypeExt.typ_of_term (get_sort (TypeExt.raw_term_sorts t)) map_sort t
   | _ => error "read_typ: ambiguous syntax");
 
-fun simple_read_typ str =
-  let fun get_sort env xi = if_none (assoc (env, xi)) [] in
-    read_typ type_syn get_sort str
-  end;
-
 
 (* read sorts *)