export: refrain from adjusting maxidx;
authorwenzelm
Sun Jul 30 21:28:55 2006 +0200 (2006-07-30)
changeset 20262ef3ee6a91c18
parent 20261 af51389aa756
child 20263 fd0ed14ba1ea
export: refrain from adjusting maxidx;
src/Pure/variable.ML
     1.1 --- a/src/Pure/variable.ML	Sun Jul 30 21:28:54 2006 +0200
     1.2 +++ b/src/Pure/variable.ML	Sun Jul 30 21:28:55 2006 +0200
     1.3 @@ -293,9 +293,8 @@
     1.4  
     1.5  fun gen_export inst inner outer ths =
     1.6    let
     1.7 -    val ths' = map Thm.adjust_maxidx_thm ths;
     1.8 -    val inner' = fold (declare_type_occs o Thm.full_prop_of) ths' inner;
     1.9 -  in map (Thm.generalize (inst inner' outer) (fold Thm.maxidx_thm ths' ~1 + 1)) ths' end;
    1.10 +    val inner' = fold (declare_type_occs o Thm.full_prop_of) ths inner;
    1.11 +  in map (Thm.generalize (inst inner' outer) (fold Thm.maxidx_thm ths ~1 + 1)) ths end;
    1.12  
    1.13  val exportT = gen_export (rpair [] oo exportT_inst);
    1.14  val export = gen_export export_inst;