# HG changeset patch
# User wenzelm
# Date 855247582 -3600
# Node ID 8b92caca102c7fd8735ac09325784b07b90b1bf4
# Parent  b386951e15e68e4bd926419929f7fbf32810bbb1
adapted read_typ, simple_read_typ;

diff -r b386951e15e6 -r 8b92caca102c src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Thu Feb 06 17:44:14 1997 +0100
+++ b/src/Pure/Syntax/syntax.ML	Thu Feb 06 17:46:22 1997 +0100
@@ -49,7 +49,8 @@
   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) -> string -> typ
+  val read_typ: syntax -> (sort * sort -> bool)
+    -> ((indexname * sort) list -> indexname -> sort) -> string -> typ
   val simple_read_typ: string -> typ
   val pretty_term: bool -> syntax -> term -> Pretty.T
   val pretty_typ: syntax -> typ -> Pretty.T
@@ -331,12 +332,15 @@
 
 (* read types *)
 
-fun read_typ syn def_sort str =
+fun read_typ syn eq_sort get_sort str =
   (case read syn typeT str of
-    [t] => typ_of_term (raw_term_sorts t) def_sort t
-  | _ => sys_error "read_typ: ambiguous type syntax");
+    [t] => typ_of_term (get_sort (raw_term_sorts eq_sort t)) t
+  | _ => error "read_typ: ambiguous type syntax");
 
-fun simple_read_typ str = read_typ type_syn (K []) str;
+fun simple_read_typ str =
+  let fun get_sort env xi = if_none (assoc (env, xi)) [] in
+    read_typ type_syn eq_set_string get_sort str
+  end;