# HG changeset patch
# User wenzelm
# Date 1120639305 -7200
# Node ID 2c1f9640b74413ef8498794ec6e02ef0d946e3b1
# Parent  3d6335ff39829805166190d4cd0ac8d1800c94a8
tuned maxidx;

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',