diff -r 3d6335ff3982 -r 2c1f9640b744 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Jul 06 10:41:44 2005 +0200
+++ b/src/Pure/thm.ML	Wed Jul 06 10:41:45 2005 +0200
@@ -352,6 +352,7 @@
 
 fun eq_tpairs ((t, u), (t', u')) = t aconv t' andalso u aconv u';
 val union_tpairs = gen_merge_lists eq_tpairs;
+val maxidx_tpairs = fold (fn (t, u) => Term.maxidx_term t o Term.maxidx_term u);
 
 fun attach_tpairs tpairs prop =
   Logic.list_implies (map Logic.mk_equals tpairs, prop);
@@ -897,7 +898,7 @@
         in
           Thm {thy_ref = thy_ref,
             der = Pt.infer_derivs' (Pt.norm_proof' env) der,
-            maxidx = maxidx_of_terms (prop' :: terms_of_tpairs tpairs'),
+            maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop'),
             shyps = may_insert_env_sorts (Theory.deref thy_ref) env shyps,
             hyps = hyps,
             tpairs = tpairs',
@@ -967,7 +968,7 @@
         else
           Thm {thy_ref = Theory.self_ref thy',
             der = Pt.infer_derivs' (Pt.instantiate vTs tpairs) der,
-            maxidx = maxidx_of_terms (prop' :: terms_of_tpairs dpairs'),
+            maxidx = maxidx_tpairs dpairs' (maxidx_of_term prop'),
             shyps = shyps',
             hyps = hyps,
             tpairs = dpairs',