# HG changeset patch
# User wenzelm
# Date 958912301 -7200
# Node ID 0281bde335ca6f82d18e08e1f8d0108e3a45aa1d
# Parent  cfc891bf7e5e2cf602fac7c81509a3356a93e3ff
added read_sort;

diff -r cfc891bf7e5e -r 0281bde335ca src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sun May 21 01:18:29 2000 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sun May 21 14:31:41 2000 +0200
@@ -51,6 +51,7 @@
   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_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
@@ -384,7 +385,7 @@
 fun read_typ syn get_sort str =
   (case read syn SynExt.typeT str of
     [t] => TypeExt.typ_of_term (get_sort (TypeExt.raw_term_sorts t)) t
-  | _ => error "read_typ: ambiguous type syntax");
+  | _ => error "read_typ: ambiguous syntax");
 
 fun simple_read_typ str =
   let fun get_sort env xi = if_none (assoc (env, xi)) [] in
@@ -392,6 +393,14 @@
   end;
 
 
+(* read sorts *)
+
+fun read_sort syn str =
+  (case read syn TypeExt.sortT str of
+    [t] => TypeExt.sort_of_term t
+  | _ => error "read_sort: ambiguous syntax");
+
+
 
 (** prepare translation rules **)