src/Pure/Isar/proof_context.ML

 (*beta normal form for terms (not eta normal form), chase variables in
   bindings environment (code taken from Pure/envir.ML)*)
 
 fun unifyT ctxt (T, U) =
   let val maxidx = Int.max (Term.maxidx_of_typ T, Term.maxidx_of_typ U)
-  in #1 (Type.unify (Sign.tsig_of (sign_of ctxt)) maxidx Vartab.empty (T, U)) end;
+  in #1 (Type.unify (Sign.tsig_of (sign_of ctxt)) (Vartab.empty, maxidx) (T, U)) end;
 
 fun norm_term (ctxt as Context {binds, ...}) schematic =
   let
     (*raised when norm has no effect on a term, to do sharing instead of copying*)
     exception SAME;

     | (sorts, TVar v) => Vartab.update (v, sorts)
     | (sorts, _) => sorts));
 
 val ins_used = foldl_term_types (fn t => foldl_atyps
   (fn (used, TFree (x, _)) => x ins_string used
-    | (used, TVar ((x, _), _)) => x ins_string used
     | (used, _) => used));
 
 val ins_occs = foldl_term_types (fn t => foldl_atyps
   (fn (tab, TFree (x, _)) => Symtab.update_multi ((x, t), tab) | (tab, _) => tab));