Type.raw_instance, Type.raw_unify, Term.zero_var_indexesT;
authorwenzelm
Thu Jul 28 15:19:53 2005 +0200 (2005-07-28)
changeset 1693693772bd33871
parent 16935 4d7f19d340e8
child 16937 0822bbdd6769
Type.raw_instance, Type.raw_unify, Term.zero_var_indexesT;
src/Pure/defs.ML
     1.1 --- a/src/Pure/defs.ML	Thu Jul 28 15:19:51 2005 +0200
     1.2 +++ b/src/Pure/defs.ML	Thu Jul 28 15:19:53 2005 +0200
     1.3 @@ -121,13 +121,13 @@
     1.4  fun subst_history s history = map (fn (ty, cn, dn) => (subst s ty, cn, dn)) history
     1.5  
     1.6  fun is_instance instance_ty general_ty =
     1.7 -    Type.typ_instance Type.empty_tsig (instance_ty, general_ty)
     1.8 +    Type.raw_instance (instance_ty, general_ty)
     1.9  
    1.10  fun is_instance_r instance_ty general_ty =
    1.11      is_instance instance_ty (rename instance_ty general_ty)
    1.12  
    1.13  fun unify ty1 ty2 =
    1.14 -    SOME (fst (Type.unify Type.empty_tsig (Vartab.empty, 0) (ty1, ty2)))
    1.15 +    SOME (Type.raw_unify (ty1, ty2) Vartab.empty)
    1.16      handle Type.TUNIFY => NONE
    1.17  
    1.18  (*
    1.19 @@ -656,7 +656,7 @@
    1.20  
    1.21  fun pretty_const pp (c, T) =
    1.22   [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
    1.23 -  Pretty.quote (Pretty.typ pp (Type.freeze_type T))];    (* FIXME zero indexes!? *)
    1.24 +  Pretty.quote (Pretty.typ pp (Type.freeze_type (Term.zero_var_indexesT T)))];
    1.25  
    1.26  fun pretty_path pp path = fold_rev (fn (T, c, def) =>
    1.27    fn [] => [Pretty.block (pretty_const pp (c, T))]