--- 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}