src/Pure/Tools/rule_insts.ML

 val partition_insts = List.partition (fn (((x, _), _), _) => String.isPrefix "'" x);
 
 fun error_var msg (xi, pos) =
   error (msg ^ quote (Term.string_of_vname xi) ^ Position.here pos);
 
-local
-
 fun the_sort tvars (xi, pos) : sort =
   (case AList.lookup (op =) tvars xi of
     SOME S => S
   | NONE => error_var "No such type variable in theorem: " (xi, pos));
 
 fun the_type vars (xi, pos) : typ =
   (case AList.lookup (op =) vars xi of
     SOME T => T
   | NONE => error_var "No such variable in theorem: " (xi, pos));
 
+local
+
 fun instantiate inst =
   Term_Subst.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #>
   Envir.beta_norm;
 
 fun make_instT f v =

     val t = Var v;
     val t' = f t;
   in if t aconv t' then NONE else SOME (t, t') end;
 
 in
+
+fun readT ctxt tvars ((xi, pos), s) =
+  let
+    val S = the_sort tvars (xi, pos);
+    val T = Syntax.read_typ ctxt s;
+  in
+    if Sign.of_sort (Proof_Context.theory_of ctxt) (T, S) then ((xi, S), T)
+    else error_var "Incompatible sort for typ instantiation of " (xi, pos)
+  end;
 
 fun read_termTs ctxt ss Ts =
   let
     fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt;
     val ts = map2 parse Ts ss;

       map2 (Type.constraint o Type_Infer.paramify_vars) Ts ts
       |> Syntax.check_terms ctxt
       |> Variable.polymorphic ctxt;
     val Ts' = map Term.fastype_of ts';
     val tyenv = fold Type.raw_match (Ts ~~ Ts') Vartab.empty;
-  in (ts', map (apsnd snd) (Vartab.dest tyenv)) end;
-
-fun read_insts ctxt mixed_insts (tvars, vars) =
-  let
-    val thy = Proof_Context.theory_of ctxt;
-
+    val tyenv' = Vartab.fold (fn (xi, (S, T)) => cons ((xi, S), T)) tyenv [];
+  in (ts', tyenv') end;
+
+fun read_insts ctxt (tvars, vars) mixed_insts =
+  let
     val (type_insts, term_insts) = partition_insts mixed_insts;
 
 
     (* type instantiations *)
 
-    fun readT ((xi, pos), s) =
-      let
-        val S = the_sort tvars (xi, pos);
-        val T = Syntax.read_typ ctxt s;
-      in
-        if Sign.of_sort thy (T, S) then ((xi, S), T)
-        else error_var "Incompatible sort for typ instantiation of " (xi, pos)
-      end;
-
-    val instT1 = Term_Subst.instantiateT (map readT type_insts);
+    val instT1 = Term_Subst.instantiateT (map (readT ctxt tvars) type_insts);
     val vars1 = map (apsnd instT1) vars;
 
 
     (* term instantiations *)
 
     val (xs, ss) = split_list term_insts;
     val Ts = map (the_type vars1) xs;
     val (ts, inferred) = read_termTs ctxt ss Ts;
 
-    val instT2 = Term.typ_subst_TVars inferred;
+    val instT2 = Term_Subst.instantiateT inferred;
     val vars2 = map (apsnd instT2) vars1;
     val inst2 = instantiate (map #1 xs ~~ ts);
 
 
     (* result *)

     val ctxt' = ctxt
       |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2
       |> Variable.declare_thm thm;
     val tvars = Thm.fold_terms Term.add_tvars thm [];
     val vars = Thm.fold_terms Term.add_vars thm [];
-    val insts = read_insts ctxt' mixed_insts (tvars, vars);
+    val insts = read_insts ctxt' (tvars, vars) mixed_insts;
   in
     Drule.instantiate_normalize insts thm
     |> singleton (Proof_Context.export ctxt' ctxt)
     |> Rule_Cases.save thm
   end;

 
 (* resolution after lifting and instantiation; may refer to parameters of the subgoal *)
 
 fun bires_inst_tac bires_flag ctxt mixed_insts thm i st = CSUBGOAL (fn (cgoal, _) =>
   let
-    val thy = Proof_Context.theory_of ctxt;
-
     val (Tinsts, tinsts) = partition_insts mixed_insts;
+
+
+    (* goal context *)
+
     val goal = Thm.term_of cgoal;
-
     val params =
       Logic.strip_params goal
       (*as they are printed: bound variables with the same name are renamed*)
       |> Term.rename_wrt_term goal
       |> rev;

       |> Variable.declare_thm thm
       |> Thm.fold_terms Variable.declare_constraints st
       |> Proof_Context.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
 
 
-    (* process type insts: Tinsts_env *)
-
-    val (rtypes, rsorts) = Drule.types_sorts thm;
-    fun readT ((xi, pos), s) =
-      let
-        val S =
-          (case rsorts xi of
-            SOME S => S
-          | NONE => error_var "No such type variable in theorem: " (xi, pos));
-        val T = Syntax.read_typ ctxt' s;
-        val U = TVar (xi, S);
-      in
-        if Sign.typ_instance thy (T, U) then (U, T)
-        else error_var "Cannot instantiate: " (xi, pos)
-      end;
-    val Tinsts_env = map readT Tinsts;
-
-
-    (* preprocess rule: extract vars and their types, apply Tinsts *)
-
-    fun get_typ (xi, pos) =
-      (case rtypes xi of
-        SOME T => typ_subst_atomic Tinsts_env T
-      | NONE => error_var "No such variable in theorem: " (xi, pos) xi);
+    (* preprocess rule *)
+
+    val tvars = Thm.fold_terms Term.add_tvars thm [];
+    val vars = Thm.fold_terms Term.add_vars thm [];
+
+    val Tinsts_env = map (readT ctxt' tvars) Tinsts;
     val (xis, ss) = split_list tinsts;
-    val Ts = map get_typ xis;
+    val Ts = map (Term_Subst.instantiateT Tinsts_env o the_type vars) xis;
 
     val (ts, envT) =
       read_termTs (Proof_Context.set_mode Proof_Context.mode_schematic ctxt') ss Ts;
-    val envT' =
-      map (fn (xi, T) => (TVar (xi, the (rsorts xi)), T)) envT @ Tinsts_env;
+    val envT' = map (fn (v, T) => (TVar v, T)) (envT @ Tinsts_env);
     val cenv =
       map (fn ((xi, _), t) => apply2 (Thm.cterm_of ctxt') (Var (xi, fastype_of t), t))
         (distinct
           (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
           (xis ~~ ts));