# HG changeset patch
# User wenzelm
# Date 1437853029 -7200
# Node ID 682c0dd89b268c70a5a69a3d0b0691ae5eb6817e
# Parent  ee811a49c8f6a8e56dd8be4f242f36a85c2ab0d2
added infer_instantiate, which is meant to supersede cterm_instantiate;

diff -r ee811a49c8f6 -r 682c0dd89b26 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Jul 24 22:29:06 2015 +0200
+++ b/src/Pure/drule.ML	Sat Jul 25 21:37:09 2015 +0200
@@ -22,6 +22,7 @@
   val implies_intr_list: cterm list -> thm -> thm
   val instantiate_normalize: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
     thm -> thm
+  val infer_instantiate: Proof.context -> (indexname * cterm) list -> thm -> thm
   val zero_var_indexes_list: thm list -> thm list
   val zero_var_indexes: thm -> thm
   val implies_intr_hyps: thm -> thm
@@ -739,6 +740,55 @@
 fun instantiate_normalize instpair th =
   Thm.adjust_maxidx_thm ~1 (Thm.instantiate instpair th COMP_INCR asm_rl);
 
+(*instantiation with type-inference for variables*)
+fun infer_instantiate _ [] th = th
+  | infer_instantiate ctxt args th =
+      let
+        val thy = Proof_Context.theory_of ctxt;
+
+        val vars = Term.add_vars (Thm.full_prop_of th) [];
+        val dups = duplicates (eq_fst op =) vars;
+        val _ = null dups orelse
+          raise THM ("infer_instantiate: inconsistent types for variables " ^
+            commas_quote (map (Syntax.string_of_term (Config.put show_types true ctxt) o Var) dups),
+            0, [th]);
+        fun var_type xi =
+          (case AList.lookup (op =) vars xi of
+            SOME T => T
+          | NONE => raise THM ("infer_instantiate: no variable " ^ string_of_indexname xi, 0, [th]));
+
+        fun infer (xi, cu) (tyenv, maxidx) =
+          let
+            val T = var_type xi;
+            val U = Thm.typ_of_cterm cu;
+            val (tyenv', maxidx') =
+              Sign.typ_unify thy (T, U)
+                (tyenv, maxidx |> Integer.max (#2 xi) |> Integer.max (Thm.maxidx_of_cterm cu))
+              handle Type.TUNIFY =>
+                let
+                  val t = Var (xi, T);
+                  val u = Thm.term_of cu;
+                in
+                  raise TYPE ("Ill-typed instantiation:\nType\n" ^
+                    Syntax.string_of_typ ctxt (Envir.norm_type tyenv T) ^
+                    "\nof variable " ^
+                    Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) t) ^
+                    "\ncannot be unified with type\n" ^
+                    Syntax.string_of_typ ctxt (Envir.norm_type tyenv U) ^ "\nof term " ^
+                    Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) u),
+                    [T, U], [t, u])
+                end;
+          in (((xi, T), cu), (tyenv', maxidx')) end;
+
+        val (args', (tyenv, _)) = fold_map infer args (Vartab.empty, 0);
+        val instT =
+          Vartab.fold (fn (xi, (S, T)) =>
+            cons ((xi, S), Thm.ctyp_of ctxt (Envir.norm_type tyenv T))) tyenv [];
+        val inst = args' |> map (fn ((xi, T), cu) =>
+          ((xi, Envir.norm_type tyenv T),
+            Thm.instantiate_cterm (instT, []) (Thm.transfer_cterm thy cu)));
+      in instantiate_normalize (instT, inst) th end;
+
 (*Left-to-right replacements: tpairs = [..., (vi, ti), ...].
   Instantiates distinct Vars by terms, inferring type instantiations.*)
 local