# HG changeset patch
# User wenzelm
# Date 1087891547 -7200
# Node ID 9606c6224933c4b439a7a51c03d78cf3f6c5d414
# Parent  aa2aaab415660375e324d350e76f2979988dc845
tuned;

diff -r aa2aaab41566 -r 9606c6224933 src/Pure/type.ML
--- a/src/Pure/type.ML	Tue Jun 22 09:52:15 2004 +0200
+++ b/src/Pure/type.ML	Tue Jun 22 10:05:47 2004 +0200
@@ -144,16 +144,17 @@
 fun bad_nargs t = "Bad number of arguments for type constructor: " ^ quote t;
 fun undecl_type c = "Undeclared type constructor: " ^ quote c;
 
+local
+
+fun inst_typ env (Type (c, Ts)) = Type (c, map (inst_typ env) Ts)
+  | inst_typ env (T as TFree (x, _)) = if_none (Library.assoc_string (env, x)) T
+  | inst_typ _ T = T;
+
 fun certify_typ normalize syntax tsig ty =
   let
     val TSig {classes, types, ...} = tsig;
     fun err msg = raise TYPE (msg, [ty], []);
 
-    fun inst_typ env (Type (c, Ts)) = Type (c, map (inst_typ env) Ts)
-      | inst_typ env (T as TFree (x, _)) = if_none (Library.assoc_string (env, x)) T
-      | inst_typ _ T = T;
-
-
     val check_syntax =
       if syntax then K ()
       else fn c => err ("Illegal occurrence of syntactic type: " ^ quote c);
@@ -181,10 +182,14 @@
     val ty' = cert ty;
   in if ty = ty' then ty else ty' end;  (*avoid copying of already normal type*)
 
+in
+
 val cert_typ         = certify_typ true false;
 val cert_typ_syntax  = certify_typ true true;
 val cert_typ_raw     = certify_typ false true;
 
+end;
+
 
 
 (** special treatment of type vars **)