src/Pure/Syntax/syntax.ML
changeset 8894 0281bde335ca
parent 8720 840c75ab2a7f
child 9372 7834e56e2277
     1.1 --- a/src/Pure/Syntax/syntax.ML	Sun May 21 01:18:29 2000 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Sun May 21 14:31:41 2000 +0200
     1.3 @@ -51,6 +51,7 @@
     1.4    val test_read: syntax -> string -> string -> unit
     1.5    val read: syntax -> typ -> string -> term list
     1.6    val read_typ: syntax -> ((indexname * sort) list -> indexname -> sort) -> string -> typ
     1.7 +  val read_sort: syntax -> string -> sort
     1.8    val simple_read_typ: string -> typ
     1.9    val pretty_term: syntax -> bool -> term -> Pretty.T
    1.10    val pretty_typ: syntax -> typ -> Pretty.T
    1.11 @@ -384,7 +385,7 @@
    1.12  fun read_typ syn get_sort str =
    1.13    (case read syn SynExt.typeT str of
    1.14      [t] => TypeExt.typ_of_term (get_sort (TypeExt.raw_term_sorts t)) t
    1.15 -  | _ => error "read_typ: ambiguous type syntax");
    1.16 +  | _ => error "read_typ: ambiguous syntax");
    1.17  
    1.18  fun simple_read_typ str =
    1.19    let fun get_sort env xi = if_none (assoc (env, xi)) [] in
    1.20 @@ -392,6 +393,14 @@
    1.21    end;
    1.22  
    1.23  
    1.24 +(* read sorts *)
    1.25 +
    1.26 +fun read_sort syn str =
    1.27 +  (case read syn TypeExt.sortT str of
    1.28 +    [t] => TypeExt.sort_of_term t
    1.29 +  | _ => error "read_sort: ambiguous syntax");
    1.30 +
    1.31 +
    1.32  
    1.33  (** prepare translation rules **)
    1.34