src/Pure/type.ML
changeset 9504 8168600e88a5
parent 8899 99266fe189a1
child 10495 284ee538991c
     1.1 --- a/src/Pure/type.ML	Thu Aug 03 00:34:22 2000 +0200
     1.2 +++ b/src/Pure/type.ML	Thu Aug 03 00:41:07 2000 +0200
     1.3 @@ -46,6 +46,7 @@
     1.4    val merge_tsigs: type_sig * type_sig -> type_sig
     1.5    val typ_errors: type_sig -> typ * string list -> string list
     1.6    val cert_typ: type_sig -> typ -> typ
     1.7 +  val cert_typ_no_norm: type_sig -> typ -> typ
     1.8    val norm_typ: type_sig -> typ -> typ
     1.9    val norm_term: type_sig -> term -> term
    1.10    val inst_term_tvars: type_sig * (indexname * typ) list -> term -> term
    1.11 @@ -352,12 +353,13 @@
    1.12  
    1.13  (* cert_typ *)           (*exception TYPE*)
    1.14  
    1.15 -(*check and normalize type wrt tsig*)
    1.16 -fun cert_typ tsig T =
    1.17 +fun cert_typ_no_norm tsig T =
    1.18    (case typ_errors tsig (T, []) of
    1.19 -    [] => norm_typ tsig T
    1.20 +    [] => T
    1.21    | errs => raise TYPE (cat_lines errs, [T], []));
    1.22  
    1.23 +fun cert_typ tsig T = norm_typ tsig (cert_typ_no_norm tsig T);
    1.24 +
    1.25  
    1.26  
    1.27  (** merge type signatures **)