--- 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 **)