src/Pure/variable.ML
changeset 20003 aac2c0d29751
parent 19926 feb4d150cfd8
child 20084 aa320957f00c
     1.1 --- a/src/Pure/variable.ML	Tue Jul 04 19:49:53 2006 +0200
     1.2 +++ b/src/Pure/variable.ML	Tue Jul 04 19:49:54 2006 +0200
     1.3 @@ -271,9 +271,8 @@
     1.4  fun gen_export inst inner outer ths =
     1.5    let
     1.6      val ths' = map Thm.adjust_maxidx_thm ths;
     1.7 -    val maxidx = fold Thm.maxidx_thm ths' ~1;
     1.8      val inner' = fold (declare_occs o Thm.full_prop_of) ths' inner;
     1.9 -  in map (Thm.generalize (inst inner' outer) (maxidx + 1)) ths' end;
    1.10 +  in map (Thm.generalize (inst inner' outer) (fold Thm.maxidx_thm ths' ~1 + 1)) ths' end;
    1.11  
    1.12  val exportT = gen_export (rpair [] oo exportT_inst);
    1.13  val export = gen_export export_inst;
    1.14 @@ -368,7 +367,12 @@
    1.15    #1 (importT_terms ts (fold declare_term ts ctxt));
    1.16  
    1.17  fun polymorphic ctxt ts =
    1.18 -  exportT_terms (fold declare_term ts ctxt) ctxt ts;
    1.19 +  let
    1.20 +    val ctxt' = fold declare_term ts ctxt;
    1.21 +    val types = subtract (op =) (used_types ctxt) (used_types ctxt');
    1.22 +    val idx = fold (Term.fold_types Term.maxidx_typ) ts ~1 + 1;
    1.23 +  in map (Term.generalize (types, []) idx) ts end;
    1.24 +
    1.25  
    1.26  
    1.27  (** term bindings **)