src/Pure/Syntax/syntax.ML
changeset 12316 79138d75405f
parent 12292 c4090cc2aa15
child 12785 27debaf2112d
     1.1 --- a/src/Pure/Syntax/syntax.ML	Wed Nov 28 23:29:48 2001 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Wed Nov 28 23:30:24 2001 +0100
     1.3 @@ -50,9 +50,9 @@
     1.4    val print_syntax: syntax -> unit
     1.5    val test_read: syntax -> string -> string -> unit
     1.6    val read: syntax -> typ -> string -> term list
     1.7 -  val read_typ: syntax -> ((indexname * sort) list -> indexname -> sort) -> string -> typ
     1.8 +  val read_typ: syntax -> ((indexname * sort) list -> indexname -> sort) -> (sort -> sort) ->
     1.9 +    string -> typ
    1.10    val read_sort: syntax -> string -> sort
    1.11 -  val simple_read_typ: string -> typ
    1.12    val pretty_term: syntax -> bool -> term -> Pretty.T
    1.13    val pretty_typ: syntax -> typ -> Pretty.T
    1.14    val pretty_sort: syntax -> sort -> Pretty.T
    1.15 @@ -371,16 +371,11 @@
    1.16  
    1.17  (* read types *)
    1.18  
    1.19 -fun read_typ syn get_sort str =
    1.20 +fun read_typ syn get_sort map_sort str =
    1.21    (case read syn SynExt.typeT str of
    1.22 -    [t] => TypeExt.typ_of_term (get_sort (TypeExt.raw_term_sorts t)) t
    1.23 +    [t] => TypeExt.typ_of_term (get_sort (TypeExt.raw_term_sorts t)) map_sort t
    1.24    | _ => error "read_typ: ambiguous syntax");
    1.25  
    1.26 -fun simple_read_typ str =
    1.27 -  let fun get_sort env xi = if_none (assoc (env, xi)) [] in
    1.28 -    read_typ type_syn get_sort str
    1.29 -  end;
    1.30 -
    1.31  
    1.32  (* read sorts *)
    1.33