diff -r 3324cbbecef8 -r 8168600e88a5 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Aug 03 00:34:22 2000 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Aug 03 00:41:07 2000 +0200
@@ -27,7 +27,9 @@
   val assumptions: context -> (cterm list * exporter) list
   val fixed_names: context -> string list
   val read_typ: context -> string -> typ
+  val read_typ_no_norm: context -> string -> typ
   val cert_typ: context -> typ -> typ
+  val cert_typ_no_norm: context -> typ -> typ
   val intern_skolem: context -> term -> term
   val extern_skolem: context -> term -> term
   val read_termTs: context -> (string * typ) list -> term list * (indexname * typ) list
@@ -377,13 +379,24 @@
 
 (** prepare types **)
 
-fun read_typ ctxt s =
-  transform_error (Sign.read_typ (sign_of ctxt, def_sort ctxt)) s
+local
+
+fun read_typ_aux read ctxt s =
+  transform_error (read (sign_of ctxt, def_sort ctxt)) s
     handle ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt);
 
-fun cert_typ ctxt raw_T =
-  Sign.certify_typ (sign_of ctxt) raw_T
-    handle TYPE (msg, _, _) => raise CONTEXT (msg, ctxt);
+fun cert_typ_aux cert ctxt raw_T = cert (sign_of ctxt) raw_T
+  handle TYPE (msg, _, _) => raise CONTEXT (msg, ctxt);
+
+in
+
+val read_typ         = read_typ_aux Sign.read_typ;
+val read_typ_no_norm = read_typ_aux Sign.read_typ_no_norm;
+val cert_typ         = cert_typ_aux Sign.certify_typ;
+val cert_typ_no_norm = cert_typ_aux Sign.certify_typ_no_norm;
+
+end;
+
 
 
 (* internalize Skolem constants *)