# HG changeset patch
# User wenzelm
# Date 1122556793 -7200
# Node ID 93772bd338716069c658197b66065e9caf2e4ac3
# Parent  4d7f19d340e827e4cdf8ee4b0f8335174860e46a
Type.raw_instance, Type.raw_unify, Term.zero_var_indexesT;

diff -r 4d7f19d340e8 -r 93772bd33871 src/Pure/defs.ML
--- a/src/Pure/defs.ML	Thu Jul 28 15:19:51 2005 +0200
+++ b/src/Pure/defs.ML	Thu Jul 28 15:19:53 2005 +0200
@@ -121,13 +121,13 @@
 fun subst_history s history = map (fn (ty, cn, dn) => (subst s ty, cn, dn)) history
 
 fun is_instance instance_ty general_ty =
-    Type.typ_instance Type.empty_tsig (instance_ty, general_ty)
+    Type.raw_instance (instance_ty, general_ty)
 
 fun is_instance_r instance_ty general_ty =
     is_instance instance_ty (rename instance_ty general_ty)
 
 fun unify ty1 ty2 =
-    SOME (fst (Type.unify Type.empty_tsig (Vartab.empty, 0) (ty1, ty2)))
+    SOME (Type.raw_unify (ty1, ty2) Vartab.empty)
     handle Type.TUNIFY => NONE
 
 (*
@@ -656,7 +656,7 @@
 
 fun pretty_const pp (c, T) =
  [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
-  Pretty.quote (Pretty.typ pp (Type.freeze_type T))];    (* FIXME zero indexes!? *)
+  Pretty.quote (Pretty.typ pp (Type.freeze_type (Term.zero_var_indexesT T)))];
 
 fun pretty_path pp path = fold_rev (fn (T, c, def) =>
   fn [] => [Pretty.block (pretty_const pp (c, T))]