typ_no_norm;

--- a/src/Pure/Isar/args.ML	Thu Aug 03 00:34:22 2000 +0200
+++ b/src/Pure/Isar/args.ML	Thu Aug 03 00:41:07 2000 +0200
@@ -30,9 +30,11 @@
   val enum1: string -> ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
   val and_list: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
   val and_list1: ('a * T list -> 'b * ('a * T list)) -> 'a * T list -> 'b list * ('a * T list)
+  val global_typ_no_norm: theory * T list -> typ * (theory * T list)
   val global_typ: theory * T list -> typ * (theory * T list)
   val global_term: theory * T list -> term * (theory * T list)
   val global_prop: theory * T list -> term * (theory * T list)
+  val local_typ_no_norm: Proof.context * T list -> typ * (Proof.context * T list)
   val local_typ: Proof.context * T list -> typ * (Proof.context * T list)
   val local_term: Proof.context * T list -> term * (Proof.context * T list)
   val local_prop: Proof.context * T list -> term * (Proof.context * T list)
@@ -137,10 +139,12 @@
 
 fun gen_item read = Scan.depend (fn st => name >> (pair st o read st));
 
+val global_typ_no_norm = gen_item (ProofContext.read_typ_no_norm o ProofContext.init);
 val global_typ = gen_item (ProofContext.read_typ o ProofContext.init);
 val global_term = gen_item (ProofContext.read_term o ProofContext.init);
 val global_prop = gen_item (ProofContext.read_prop o ProofContext.init);
 
+val local_typ_no_norm = gen_item ProofContext.read_typ_no_norm;
 val local_typ = gen_item ProofContext.read_typ;
 val local_term = gen_item ProofContext.read_term;
 val local_prop = gen_item ProofContext.read_prop;

--- a/src/Pure/Isar/isar_output.ML	Thu Aug 03 00:34:22 2000 +0200
+++ b/src/Pure/Isar/isar_output.ML	Thu Aug 03 00:41:07 2000 +0200
@@ -288,7 +288,7 @@
  [("thm", args Attrib.local_thms (string_of oo pretty_thm)),
   ("prop", args Args.local_prop (string_of oo pretty_term)),
   ("term", args Args.local_term (string_of oo pretty_term)),
-  ("typ", args Args.local_typ (string_of oo pretty_typ))];
+  ("typ", args Args.local_typ_no_norm (string_of oo pretty_typ))];
 
 end;
 

--- 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 *)

--- a/src/Pure/sign.ML	Thu Aug 03 00:34:22 2000 +0200
+++ b/src/Pure/sign.ML	Thu Aug 03 00:41:07 2000 +0200
@@ -84,10 +84,12 @@
   val certify_class: sg -> class -> class
   val certify_sort: sg -> sort -> sort
   val certify_typ: sg -> typ -> typ
+  val certify_typ_no_norm: sg -> typ -> typ
   val certify_term: sg -> term -> term * typ * int
   val read_sort: sg -> string -> sort
   val read_raw_typ: sg * (indexname -> sort option) -> string -> typ
   val read_typ: sg * (indexname -> sort option) -> string -> typ
+  val read_typ_no_norm: sg * (indexname -> sort option) -> string -> typ
   val infer_types: sg -> (indexname -> typ option) ->
     (indexname -> sort option) -> string list -> bool
     -> xterm list * typ -> term * (indexname * typ) list
@@ -576,9 +578,14 @@
   (check_stale sg; rd_raw_typ syn tsig spaces def_sort str);
 
 (*read and certify typ wrt a signature*)
-fun read_typ (sg, def_sort) str =
-  (Type.cert_typ (tsig_of sg) (read_raw_typ (sg, def_sort) str)
-      handle TYPE (msg, _, _) => (error_msg msg; err_in_type str));
+local
+  fun read_typ_aux cert (sg, def_sort) str =
+    (cert (tsig_of sg) (read_raw_typ (sg, def_sort) str)
+        handle TYPE (msg, _, _) => (error_msg msg; err_in_type str));
+in
+  val read_typ = read_typ_aux Type.cert_typ;
+  val read_typ_no_norm = read_typ_aux Type.cert_typ_no_norm;
+end;
 
 
 
@@ -587,6 +594,7 @@
 val certify_class = Type.cert_class o tsig_of;
 val certify_sort = Type.cert_sort o tsig_of;
 val certify_typ = Type.cert_typ o tsig_of;
+val certify_typ_no_norm = Type.cert_typ_no_norm o tsig_of;
 
 
 (* certify_term *)

--- 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 **)