src/Pure/variable.ML
changeset 20509 073a5ed7dd71
parent 20303 e25d5a2a50bc
child 20579 4dc799edef89
     1.1 --- a/src/Pure/variable.ML	Tue Sep 12 12:12:39 2006 +0200
     1.2 +++ b/src/Pure/variable.ML	Tue Sep 12 12:12:46 2006 +0200
     1.3 @@ -322,19 +322,19 @@
     1.4  fun exportT_inst inner outer = #1 (export_inst inner outer);
     1.5  
     1.6  fun exportT_terms inner outer ts =
     1.7 -  map (Term.generalize (exportT_inst (fold declare_type_occs ts inner) outer, [])
     1.8 +  map (TermSubst.generalize (exportT_inst (fold declare_type_occs ts inner) outer, [])
     1.9      (fold (Term.fold_types Term.maxidx_typ) ts ~1 + 1)) ts;
    1.10  
    1.11  fun export_terms inner outer ts =
    1.12 -  map (Term.generalize (export_inst (fold declare_type_occs ts inner) outer)
    1.13 +  map (TermSubst.generalize (export_inst (fold declare_type_occs ts inner) outer)
    1.14      (fold Term.maxidx_term ts ~1 + 1)) ts;
    1.15  
    1.16  fun export_prf inner outer prf =
    1.17    let
    1.18      val insts = export_inst (declare_prf prf inner) outer;
    1.19      val idx = Proofterm.maxidx_proof prf ~1 + 1;
    1.20 -    val gen_term = Term.generalize_option insts idx;
    1.21 -    val gen_typ = Term.generalizeT_option (#1 insts) idx;
    1.22 +    val gen_term = TermSubst.generalize_option insts idx;
    1.23 +    val gen_typ = TermSubst.generalizeT_option (#1 insts) idx;
    1.24    in Proofterm.map_proof_terms_option gen_term gen_typ prf end;
    1.25  
    1.26  fun gen_export inst inner outer ths =
    1.27 @@ -359,18 +359,18 @@
    1.28    let
    1.29      val ren = if is_open then I else Name.internal;
    1.30      val (instT, ctxt') = importT_inst ts ctxt;
    1.31 -    val vars = map (apsnd (Term.instantiateT instT)) (rev (fold Term.add_vars ts []));
    1.32 +    val vars = map (apsnd (TermSubst.instantiateT instT)) (rev (fold Term.add_vars ts []));
    1.33      val (xs, ctxt'') = invent_fixes (map (ren o #1 o #1) vars) ctxt';
    1.34      val inst = vars ~~ map Free (xs ~~ map #2 vars);
    1.35    in ((instT, inst), ctxt'') end;
    1.36  
    1.37  fun importT_terms ts ctxt =
    1.38    let val (instT, ctxt') = importT_inst ts ctxt
    1.39 -  in (map (Term.instantiate (instT, [])) ts, ctxt') end;
    1.40 +  in (map (TermSubst.instantiate (instT, [])) ts, ctxt') end;
    1.41  
    1.42  fun import_terms is_open ts ctxt =
    1.43    let val (inst, ctxt') = import_inst is_open ts ctxt
    1.44 -  in (map (Term.instantiate inst) ts, ctxt') end;
    1.45 +  in (map (TermSubst.instantiate inst) ts, ctxt') end;
    1.46  
    1.47  fun importT ths ctxt =
    1.48    let
    1.49 @@ -472,6 +472,6 @@
    1.50      val occs' = type_occs_of ctxt';
    1.51      val types = Symtab.fold (fn (a, _) => if Symtab.defined occs a then I else cons a) occs' [];
    1.52      val idx = fold (Term.fold_types Term.maxidx_typ) ts ~1 + 1;
    1.53 -  in map (Term.generalize (types, []) idx) ts end;
    1.54 +  in map (TermSubst.generalize (types, []) idx) ts end;
    1.55  
    1.56  end;