--- a/src/Pure/type.ML Thu Aug 03 00:34:22 2000 +0200
+++ b/src/Pure/type.ML Thu Aug 03 00:41:07 2000 +0200
@@ -46,6 +46,7 @@
val merge_tsigs: type_sig * type_sig -> type_sig
val typ_errors: type_sig -> typ * string list -> string list
val cert_typ: type_sig -> typ -> typ
+ val cert_typ_no_norm: type_sig -> typ -> typ
val norm_typ: type_sig -> typ -> typ
val norm_term: type_sig -> term -> term
val inst_term_tvars: type_sig * (indexname * typ) list -> term -> term
@@ -352,12 +353,13 @@
(* cert_typ *) (*exception TYPE*)
-(*check and normalize type wrt tsig*)
-fun cert_typ tsig T =
+fun cert_typ_no_norm tsig T =
(case typ_errors tsig (T, []) of
- [] => norm_typ tsig T
+ [] => T
| errs => raise TYPE (cat_lines errs, [T], []));
+fun cert_typ tsig T = norm_typ tsig (cert_typ_no_norm tsig T);
+
(** merge type signatures **)