src/Pure/Isar/method.ML

           ("No such variable in theorem: " ^ Syntax.string_of_vname xi);
     val (rtypes, rsorts) = types_sorts thm;
     fun readT (xi, s) =
         let val S = case rsorts xi of SOME S => S | NONE => absent xi;
             val T = Sign.read_typ (sign, sorts) s;
-        in if Sign.typ_instance sign (T, TVar (xi, S)) then (xi, T)
+            val U = TVar (xi, S);
+        in if Sign.typ_instance sign (T, U) then (U, T)
            else error
              ("Instantiation of " ^ Syntax.string_of_vname xi ^ " fails")
         end;
     val Tinsts_env = map readT Tinsts;
     (* Preprocess rule: extract vars and their types, apply Tinsts *)
     fun get_typ xi =
       (case rtypes xi of
-           SOME T => typ_subst_TVars Tinsts_env T
+           SOME T => typ_subst_atomic Tinsts_env T
          | NONE => absent xi);
     val (xis, ss) = Library.split_list tinsts;
     val Ts = map get_typ xis;
         val (_, _, Bi, _) = dest_state(st,i)
         val params = Logic.strip_params Bi

           | types' xi = types xi;
         fun internal x = isSome (types' (x, ~1));
         val used = Drule.add_used thm (Drule.add_used st []);
         val (ts, envT) =
           ProofContext.read_termTs_schematic ctxt internal types' sorts used (ss ~~ Ts);
-        val cenvT = map (apsnd (Thm.ctyp_of sign)) (envT @ Tinsts_env);
+        val envT' = map (fn (ixn, T) =>
+          (TVar (ixn, valOf (rsorts ixn)), T)) envT @ Tinsts_env;
         val cenv =
           map
             (fn (xi, t) =>
               pairself (Thm.cterm_of sign) (Var (xi, fastype_of t), t))
             (gen_distinct

           | liftvar t = raise TERM("Variable expected", [t]);
         fun liftterm t = list_abs_free
               (params, Logic.incr_indexes(paramTs,inc) t)
         fun liftpair (cv,ct) =
               (cterm_fun liftvar cv, cterm_fun liftterm ct)
-        fun lifttvar((a,i),ctyp) =
-            let val {T,sign} = rep_ctyp ctyp
-            in  ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end
+        val lifttvar = pairself (ctyp_of sign o incr_tvar inc);
         val rule = Drule.instantiate
-              (map lifttvar cenvT, map liftpair cenv)
+              (map lifttvar envT', map liftpair cenv)
               (lift_rule (st, i) thm)
       in
         if i > nprems_of st then no_tac st
         else st |>
           compose_tac (bires_flag, rule, nprems_of thm) i