src/Pure/variable.ML
changeset 22671 3c62305fbee6
parent 22601 948f23d4af29
child 22691 290454649b8c
     1.1 --- a/src/Pure/variable.ML	Sat Apr 14 00:46:20 2007 +0200
     1.2 +++ b/src/Pure/variable.ML	Sat Apr 14 00:46:21 2007 +0200
     1.3 @@ -35,8 +35,6 @@
     1.4    val auto_fixes: term -> Proof.context -> Proof.context
     1.5    val variant_fixes: string list -> Proof.context -> string list * Proof.context
     1.6    val invent_types: sort list -> Proof.context -> (string * sort) list * Proof.context
     1.7 -  val export_inst: Proof.context -> Proof.context -> string list * string list
     1.8 -  val exportT_inst: Proof.context -> Proof.context -> string list
     1.9    val export_terms: Proof.context -> Proof.context -> term list -> term list
    1.10    val exportT_terms: Proof.context -> Proof.context -> term list -> term list
    1.11    val exportT: Proof.context -> Proof.context -> thm list -> thm list
    1.12 @@ -161,10 +159,12 @@
    1.13  
    1.14  (* type occurrences *)
    1.15  
    1.16 -val declare_type_occs = map_type_occs o fold_term_types
    1.17 +val decl_type_occs = fold_term_types
    1.18    (fn Free (x, _) => fold_atyps (fn TFree (a, _) => Symtab.insert_list (op =) (a, x) | _ => I)
    1.19      | _ => fold_atyps (fn TFree (a, _) => Symtab.default (a, []) | _ => I));
    1.20  
    1.21 +val declare_type_occs = map_type_occs o decl_type_occs;
    1.22 +
    1.23  
    1.24  (* constraints *)
    1.25  
    1.26 @@ -302,7 +302,7 @@
    1.27  
    1.28  
    1.29  
    1.30 -(** export -- generalize type/term variables **)
    1.31 +(** export -- generalize type/term variables (beware of closure sizes) **)
    1.32  
    1.33  fun export_inst inner outer =
    1.34    let
    1.35 @@ -312,37 +312,48 @@
    1.36  
    1.37      val gen_fixes = map #2 (Library.take (length fixes_inner - length fixes_outer, fixes_inner));
    1.38      val still_fixed = not o member (op =) gen_fixes;
    1.39 -    val gen_fixesT =
    1.40 +
    1.41 +    val type_occs_inner = type_occs_of inner;
    1.42 +    fun gen_fixesT ts =
    1.43        Symtab.fold (fn (a, xs) =>
    1.44          if declared_outer a orelse exists still_fixed xs
    1.45 -        then I else cons a) (type_occs_of inner) [];
    1.46 +        then I else cons a) (fold decl_type_occs ts type_occs_inner) [];
    1.47    in (gen_fixesT, gen_fixes) end;
    1.48  
    1.49  fun exportT_inst inner outer = #1 (export_inst inner outer);
    1.50  
    1.51 -fun exportT_terms inner outer ts =
    1.52 -  map (TermSubst.generalize (exportT_inst (fold declare_type_occs ts inner) outer, [])
    1.53 -    (fold (Term.fold_types Term.maxidx_typ) ts ~1 + 1)) ts;
    1.54 +fun exportT_terms inner outer =
    1.55 +  let val mk_tfrees = exportT_inst inner outer in
    1.56 +    fn ts => ts |> map
    1.57 +      (TermSubst.generalize (mk_tfrees ts, [])
    1.58 +        (fold (Term.fold_types Term.maxidx_typ) ts ~1 + 1))
    1.59 +  end;
    1.60  
    1.61 -fun export_terms inner outer ts =
    1.62 -  map (TermSubst.generalize (export_inst (fold declare_type_occs ts inner) outer)
    1.63 -    (fold Term.maxidx_term ts ~1 + 1)) ts;
    1.64 +fun export_terms inner outer =
    1.65 +  let val (mk_tfrees, tfrees) = export_inst inner outer in
    1.66 +    fn ts => ts |> map
    1.67 +      (TermSubst.generalize (mk_tfrees ts, tfrees)
    1.68 +        (fold Term.maxidx_term ts ~1 + 1))
    1.69 +  end;
    1.70  
    1.71  fun export_prf inner outer prf =
    1.72    let
    1.73 -    val insts = export_inst (declare_prf prf inner) outer;
    1.74 +    val (mk_tfrees, frees) = export_inst (declare_prf prf inner) outer;
    1.75 +    val tfrees = mk_tfrees [];
    1.76      val idx = Proofterm.maxidx_proof prf ~1 + 1;
    1.77 -    val gen_term = TermSubst.generalize_option insts idx;
    1.78 -    val gen_typ = TermSubst.generalizeT_option (#1 insts) idx;
    1.79 +    val gen_term = TermSubst.generalize_option (tfrees, frees) idx;
    1.80 +    val gen_typ = TermSubst.generalizeT_option tfrees idx;
    1.81    in Proofterm.map_proof_terms_option gen_term gen_typ prf end;
    1.82  
    1.83 -fun gen_export inst inner outer ths =
    1.84 +
    1.85 +fun gen_export (mk_tfrees, frees) ths =
    1.86    let
    1.87 -    val inner' = fold (declare_type_occs o Thm.full_prop_of) ths inner;
    1.88 -  in map (Thm.generalize (inst inner' outer) (fold Thm.maxidx_thm ths ~1 + 1)) ths end;
    1.89 +    val tfrees = mk_tfrees (map Thm.full_prop_of ths);
    1.90 +    val maxidx = fold Thm.maxidx_thm ths ~1;
    1.91 +  in map (Thm.generalize (tfrees, frees) (maxidx + 1)) ths end;
    1.92  
    1.93 -val exportT = gen_export (rpair [] oo exportT_inst);
    1.94 -val export = gen_export export_inst;
    1.95 +fun exportT inner outer = gen_export (exportT_inst inner outer, []);
    1.96 +fun export inner outer = gen_export (export_inst inner outer);
    1.97  
    1.98  fun export_morphism inner outer =
    1.99    let