# HG changeset patch
# User wenzelm
# Date 1085167272 -7200
# Node ID 949a3f558a437c1871d490e3eb5272c43023fcac
# Parent  e15d4bd7fe717bd703589febe2645a2261cde6eb
xxx_typ_raw replace xxx_typ_no_norm forms;

diff -r e15d4bd7fe71 -r 949a3f558a43 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Fri May 21 21:20:38 2004 +0200
+++ b/src/Pure/Isar/args.ML	Fri May 21 21:21:12 2004 +0200
@@ -40,11 +40,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_raw: 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_raw: 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)
@@ -171,12 +171,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_raw = gen_item (ProofContext.read_typ_raw 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_raw = gen_item ProofContext.read_typ_raw;
 val local_typ = gen_item ProofContext.read_typ;
 val local_term = gen_item ProofContext.read_term;
 val local_prop = gen_item ProofContext.read_prop;
diff -r e15d4bd7fe71 -r 949a3f558a43 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri May 21 21:20:38 2004 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri May 21 21:21:12 2004 +0200
@@ -25,9 +25,9 @@
   val default_type: context -> string -> typ option
   val used_types: context -> string list
   val read_typ: context -> string -> typ
-  val read_typ_no_norm: context -> string -> typ
+  val read_typ_raw: context -> string -> typ
   val cert_typ: context -> typ -> typ
-  val cert_typ_no_norm: context -> typ -> typ
+  val cert_typ_raw: context -> typ -> typ
   val get_skolem: context -> string -> string
   val extern_skolem: context -> term -> term
   val read_termTs: context -> (string -> bool) -> (indexname -> typ option)
@@ -413,10 +413,10 @@
 
 (* Read/certify type, using default sort information from context. *)
 
-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;
+val read_typ     = read_typ_aux Sign.read_typ';
+val read_typ_raw = read_typ_aux Sign.read_typ_raw';
+val cert_typ     = cert_typ_aux Sign.certify_typ;
+val cert_typ_raw = cert_typ_aux Sign.certify_typ_raw;
 
 end;