# HG changeset patch
# User wenzelm
# Date 1154287735 -7200
# Node ID ef3ee6a91c181a6f837544b4da2c01d2703ddb6c
# Parent  af51389aa75662bb1810c0cf5c0aaa7c0fcbc5e3
export: refrain from adjusting maxidx;

diff -r af51389aa756 -r ef3ee6a91c18 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Sun Jul 30 21:28:54 2006 +0200
+++ b/src/Pure/variable.ML	Sun Jul 30 21:28:55 2006 +0200
@@ -293,9 +293,8 @@
 
 fun gen_export inst inner outer ths =
   let
-    val ths' = map Thm.adjust_maxidx_thm ths;
-    val inner' = fold (declare_type_occs o Thm.full_prop_of) ths' inner;
-  in map (Thm.generalize (inst inner' outer) (fold Thm.maxidx_thm ths' ~1 + 1)) ths' end;
+    val inner' = fold (declare_type_occs o Thm.full_prop_of) ths inner;
+  in map (Thm.generalize (inst inner' outer) (fold Thm.maxidx_thm ths ~1 + 1)) ths end;
 
 val exportT = gen_export (rpair [] oo exportT_inst);
 val export = gen_export export_inst;