src/Pure/Tools/rule_insts.ML

--- a/src/Pure/Tools/rule_insts.ML	Thu Mar 19 22:31:23 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML	Fri Mar 20 11:09:08 2015 +0100
@@ -48,8 +48,6 @@
 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
@@ -60,6 +58,8 @@
     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;
@@ -78,6 +78,15 @@
 
 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;
@@ -88,27 +97,17 @@
       |> 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;
+    val tyenv' = Vartab.fold (fn (xi, (S, T)) => cons ((xi, S), T)) tyenv [];
+  in (ts', tyenv') end;
 
-fun read_insts ctxt mixed_insts (tvars, vars) =
+fun read_insts ctxt (tvars, vars) mixed_insts =
   let
-    val thy = Proof_Context.theory_of ctxt;
-
     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;
 
 
@@ -118,7 +117,7 @@
     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);
 
@@ -139,7 +138,7 @@
       |> 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)
@@ -212,11 +211,12 @@
 
 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;
+
 
-    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*)
@@ -228,37 +228,18 @@
       |> Proof_Context.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params);
 
 
-    (* process type insts: Tinsts_env *)
+    (* preprocess rule *)
 
-    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;
+    val tvars = Thm.fold_terms Term.add_tvars thm [];
+    val vars = Thm.fold_terms Term.add_vars thm [];
 
-
-    (* 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);
+    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