# HG changeset patch
# User wenzelm
# Date 1437989410 -7200
# Node ID c24fa03f4c71b7ceb689c328cf06e230cdb9f5fe
# Parent  f21f70d24844094102e8390cc1b935d38eadc357
tuned signature;

diff -r f21f70d24844 -r c24fa03f4c71 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Jul 27 00:17:18 2015 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Jul 27 11:30:10 2015 +0200
@@ -106,7 +106,7 @@
     val th = EXCLUDED_MIDDLE
     val [vx] = Term.add_vars (Thm.prop_of th) []
   in
-    infer_instantiate_vars ctxt [(vx, Thm.cterm_of ctxt i_atom)] th
+    infer_instantiate_types ctxt [(vx, Thm.cterm_of ctxt i_atom)] th
   end
 
 fun assume_inference ctxt type_enc concealed sym_tab atom =
@@ -162,7 +162,7 @@
           Syntax.string_of_term ctxt (Thm.term_of x) ^ " |-> " ^
           Syntax.string_of_term ctxt (Thm.term_of y)))))
   in
-    infer_instantiate_vars ctxt (map (apfst (dest_Var o Thm.term_of)) substs') i_th
+    infer_instantiate_types ctxt (map (apfst (dest_Var o Thm.term_of)) substs') i_th
   end
   handle THM (msg, _, _) => raise METIS_RECONSTRUCT ("inst_inference", msg)
        | ERROR msg => raise METIS_RECONSTRUCT ("inst_inference", msg)
@@ -308,7 +308,7 @@
     val i_t = singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) t
     val _ = trace_msg ctxt (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
     val c_t = cterm_incr_types ctxt refl_idx i_t
-  in infer_instantiate_vars ctxt [(dest_Var (Thm.term_of refl_x), c_t)] REFL_THM end
+  in infer_instantiate_types ctxt [(dest_Var (Thm.term_of refl_x), c_t)] REFL_THM end
 
 (* INFERENCE RULE: EQUALITY *)
 
@@ -374,7 +374,7 @@
         map (apply2 (Thm.cterm_of ctxt))
           (ListPair.zip (Misc_Legacy.term_vars (Thm.prop_of subst'), [tm_abs, tm_subst, i_tm]))
   in
-    infer_instantiate_vars ctxt (map (apfst (dest_Var o Thm.term_of)) eq_terms) subst'
+    infer_instantiate_types ctxt (map (apfst (dest_Var o Thm.term_of)) eq_terms) subst'
   end
 
 val factor = Seq.hd o distinct_subgoals_tac
@@ -520,7 +520,7 @@
       [] |> try (unify_terms (prem, concl) #> map (apply2 (Thm.cterm_of ctxt)))
          |> the_default [] (* FIXME *)
   in
-    infer_instantiate_vars ctxt (map (apfst (dest_Var o Thm.term_of)) t_inst) th
+    infer_instantiate_types ctxt (map (apfst (dest_Var o Thm.term_of)) t_inst) th
   end
 
 val copy_prem = @{lemma "P ==> (P ==> P ==> Q) ==> Q" by fast}
diff -r f21f70d24844 -r c24fa03f4c71 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Mon Jul 27 00:17:18 2015 +0200
+++ b/src/Pure/drule.ML	Mon Jul 27 11:30:10 2015 +0200
@@ -22,7 +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_vars: Proof.context -> ((indexname * typ) * cterm) list -> thm -> thm
+  val infer_instantiate_types: Proof.context -> ((indexname * typ) * cterm) list -> thm -> thm
   val infer_instantiate: Proof.context -> (indexname * cterm) list -> thm -> thm
   val cterm_instantiate: (cterm * cterm) list -> thm -> thm
   val instantiate': ctyp option list -> cterm option list -> thm -> thm
@@ -743,8 +743,8 @@
   Thm.adjust_maxidx_thm ~1 (Thm.instantiate instpair th COMP_INCR asm_rl);
 
 (*instantiation with type-inference for variables*)
-fun infer_instantiate_vars _ [] th = th
-  | infer_instantiate_vars ctxt args th =
+fun infer_instantiate_types _ [] th = th
+  | infer_instantiate_types ctxt args th =
       let
         val thy = Proof_Context.theory_of ctxt;
 
@@ -761,7 +761,7 @@
                   val t = Var (xi, T);
                   val u = Thm.term_of cu;
                 in
-                  raise THM ("infer_instantiate: type " ^
+                  raise THM ("infer_instantiate_types: type " ^
                     Syntax.string_of_typ ctxt (Envir.norm_type tyenv T) ^ " of variable " ^
                     Syntax.string_of_term ctxt (Term.map_types (Envir.norm_type tyenv) t) ^
                     "\ncannot be unified with type " ^
@@ -794,7 +794,7 @@
             0, [th]);
         val args' = args |> map_filter (fn (xi, cu) =>
           AList.lookup (op =) vars xi |> Option.map (fn T => ((xi, T), cu)));
-      in infer_instantiate_vars ctxt args' th end;
+      in infer_instantiate_types ctxt args' th end;
 
 (*Left-to-right replacements: tpairs = [..., (vi, ti), ...].
   Instantiates distinct Vars by terms, inferring type instantiations.*)
@@ -856,7 +856,7 @@
     val args' = zip_options vars args
       handle ListPair.UnequalLengths =>
         raise THM ("infer_instantiate': more instantiations than variables in thm", 0, [th]);
-  in infer_instantiate_vars ctxt args' th end;
+  in infer_instantiate_types ctxt args' th end;