# HG changeset patch
# User wenzelm
# Date 1565625646 -7200
# Node ID c04e2426f319e0e69c4a856620103c7218e309ad
# Parent  7a63b16c53c44109c2c329429d8b6bcc6ecc3f21
tuned;

diff -r 7a63b16c53c4 -r c04e2426f319 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Aug 12 17:15:41 2019 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Aug 12 18:00:46 2019 +0200
@@ -152,7 +152,7 @@
     val (vars, tms) =
       ListPair.unzip (map_filter subst_translation substs)
       ||> polish_hol_terms ctxt concealed
-    val ctm_of = cterm_incr_types ctxt (1 + Thm.maxidx_of i_th)
+    val ctm_of = cterm_incr_types ctxt (Thm.maxidx_of i_th + 1)
     val substs' = ListPair.zip (vars, map ctm_of tms)
     val _ = trace_msg ctxt (fn () =>
       cat_lines ("subst_translations:" ::
@@ -182,7 +182,7 @@
   Instantiations of those Vars could then fail.*)
 fun resolve_inc_tyvars ctxt tha i thb =
   let
-    val tha = incr_type_indexes ctxt (1 + Thm.maxidx_of thb) tha
+    val tha = incr_type_indexes ctxt (Thm.maxidx_of thb + 1) tha
     fun res (tha, thb) =
       (case Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = true}
             (false, tha, Thm.nprems_of tha) i thb
@@ -299,15 +299,13 @@
 (* INFERENCE RULE: REFL *)
 
 val REFL_THM = Thm.incr_indexes 2 @{lemma "x \<noteq> x \<Longrightarrow> False" by (drule notE) (rule refl)}
-
 val [refl_x] = Term.add_vars (Thm.prop_of REFL_THM) [];
-val refl_idx = 1 + Thm.maxidx_of REFL_THM;
 
 fun refl_inference ctxt type_enc concealed sym_tab t =
   let
     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
+    val c_t = cterm_incr_types ctxt (Thm.maxidx_of REFL_THM + 1) i_t
   in infer_instantiate_types ctxt [(refl_x, c_t)] REFL_THM end
 
 
@@ -368,8 +366,8 @@
     val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
     val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
     val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
-    val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill-typed but gives right max*)
-    val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
+    val maxidx = fold Term.maxidx_term [i_tm, tm_abs, tm_subst] ~1
+    val subst' = Thm.incr_indexes (maxidx + 1) (if pos then subst_em else ssubst_em)
     val _ = trace_msg ctxt (fn () => "subst' " ^ Thm.string_of_thm ctxt subst')
     val eq_terms =
       map (apply2 (Thm.cterm_of ctxt))