src/Pure/type.ML
changeset 14998 9606c6224933
parent 14993 802f3732a54e
child 15531 08c8dad8e399
     1.1 --- a/src/Pure/type.ML	Tue Jun 22 09:52:15 2004 +0200
     1.2 +++ b/src/Pure/type.ML	Tue Jun 22 10:05:47 2004 +0200
     1.3 @@ -144,16 +144,17 @@
     1.4  fun bad_nargs t = "Bad number of arguments for type constructor: " ^ quote t;
     1.5  fun undecl_type c = "Undeclared type constructor: " ^ quote c;
     1.6  
     1.7 +local
     1.8 +
     1.9 +fun inst_typ env (Type (c, Ts)) = Type (c, map (inst_typ env) Ts)
    1.10 +  | inst_typ env (T as TFree (x, _)) = if_none (Library.assoc_string (env, x)) T
    1.11 +  | inst_typ _ T = T;
    1.12 +
    1.13  fun certify_typ normalize syntax tsig ty =
    1.14    let
    1.15      val TSig {classes, types, ...} = tsig;
    1.16      fun err msg = raise TYPE (msg, [ty], []);
    1.17  
    1.18 -    fun inst_typ env (Type (c, Ts)) = Type (c, map (inst_typ env) Ts)
    1.19 -      | inst_typ env (T as TFree (x, _)) = if_none (Library.assoc_string (env, x)) T
    1.20 -      | inst_typ _ T = T;
    1.21 -
    1.22 -
    1.23      val check_syntax =
    1.24        if syntax then K ()
    1.25        else fn c => err ("Illegal occurrence of syntactic type: " ^ quote c);
    1.26 @@ -181,10 +182,14 @@
    1.27      val ty' = cert ty;
    1.28    in if ty = ty' then ty else ty' end;  (*avoid copying of already normal type*)
    1.29  
    1.30 +in
    1.31 +
    1.32  val cert_typ         = certify_typ true false;
    1.33  val cert_typ_syntax  = certify_typ true true;
    1.34  val cert_typ_raw     = certify_typ false true;
    1.35  
    1.36 +end;
    1.37 +
    1.38  
    1.39  
    1.40  (** special treatment of type vars **)