adapted read_typ, simple_read_typ;
authorwenzelm
Thu Feb 06 17:46:22 1997 +0100 (1997-02-06)
changeset 25858b92caca102c
parent 2584 b386951e15e6
child 2586 c7a0c0618ca0
adapted read_typ, simple_read_typ;
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/syntax.ML	Thu Feb 06 17:44:14 1997 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Thu Feb 06 17:46:22 1997 +0100
     1.3 @@ -49,7 +49,8 @@
     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) -> string -> typ
     1.8 +  val read_typ: syntax -> (sort * sort -> bool)
     1.9 +    -> ((indexname * sort) list -> indexname -> sort) -> string -> typ
    1.10    val simple_read_typ: string -> typ
    1.11    val pretty_term: bool -> syntax -> term -> Pretty.T
    1.12    val pretty_typ: syntax -> typ -> Pretty.T
    1.13 @@ -331,12 +332,15 @@
    1.14  
    1.15  (* read types *)
    1.16  
    1.17 -fun read_typ syn def_sort str =
    1.18 +fun read_typ syn eq_sort get_sort str =
    1.19    (case read syn typeT str of
    1.20 -    [t] => typ_of_term (raw_term_sorts t) def_sort t
    1.21 -  | _ => sys_error "read_typ: ambiguous type syntax");
    1.22 +    [t] => typ_of_term (get_sort (raw_term_sorts eq_sort t)) t
    1.23 +  | _ => error "read_typ: ambiguous type syntax");
    1.24  
    1.25 -fun simple_read_typ str = read_typ type_syn (K []) str;
    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 eq_set_string get_sort str
    1.29 +  end;
    1.30  
    1.31  
    1.32