moved term subst functions to TermSubst;
authorwenzelm
Tue Sep 12 12:12:46 2006 +0200 (2006-09-12)
changeset 20509073a5ed7dd71
parent 20508 8182d961c7cc
child 20510 5e844572939d
moved term subst functions to TermSubst;
src/Pure/Isar/rule_insts.ML
src/Pure/consts.ML
src/Pure/drule.ML
src/Pure/proofterm.ML
src/Pure/variable.ML
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Tue Sep 12 12:12:39 2006 +0200
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Tue Sep 12 12:12:46 2006 +0200
     1.3 @@ -40,7 +40,7 @@
     1.4    end;
     1.5  
     1.6  fun instantiate inst =
     1.7 -  Term.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #>
     1.8 +  TermSubst.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #>
     1.9    Envir.beta_norm;
    1.10  
    1.11  fun make_instT f v =
    1.12 @@ -88,7 +88,7 @@
    1.13        end;
    1.14  
    1.15      val type_insts1 = map readT type_insts;
    1.16 -    val instT1 = Term.instantiateT type_insts1;
    1.17 +    val instT1 = TermSubst.instantiateT type_insts1;
    1.18      val vars1 = map (apsnd instT1) vars;
    1.19  
    1.20  
     2.1 --- a/src/Pure/consts.ML	Tue Sep 12 12:12:39 2006 +0200
     2.2 +++ b/src/Pure/consts.ML	Tue Sep 12 12:12:46 2006 +0200
     2.3 @@ -177,7 +177,7 @@
     2.4    let
     2.5      val declT = declaration consts c;
     2.6      val vars = map Term.dest_TVar (typargs consts (c, declT));
     2.7 -  in declT |> Term.instantiateT (vars ~~ Ts) end;
     2.8 +  in declT |> TermSubst.instantiateT (vars ~~ Ts) end;
     2.9  
    2.10  
    2.11  
     3.1 --- a/src/Pure/drule.ML	Tue Sep 12 12:12:39 2006 +0200
     3.2 +++ b/src/Pure/drule.ML	Tue Sep 12 12:12:46 2006 +0200
     3.3 @@ -396,7 +396,7 @@
     3.4    let
     3.5      val thy = Thm.theory_of_thm th;
     3.6      val certT = Thm.ctyp_of thy and cert = Thm.cterm_of thy;
     3.7 -    val (instT, inst) = Term.zero_var_indexes_inst (Thm.full_prop_of th);
     3.8 +    val (instT, inst) = TermSubst.zero_var_indexes_inst (Thm.full_prop_of th);
     3.9      val cinstT = map (fn (v, T) => (certT (TVar v), certT T)) instT;
    3.10      val cinst = map (fn (v, t) => (cert (Var v), cert t)) inst;
    3.11    in Thm.adjust_maxidx_thm ~1 (Thm.instantiate (cinstT, cinst) th) end;
    3.12 @@ -914,7 +914,7 @@
    3.13      val instT0 = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S)));
    3.14      val instT = map (fn (v, T) => (certT (TVar v), certT T)) instT0;
    3.15      val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) =>
    3.16 -      let val T' = Term.instantiateT instT0 T
    3.17 +      let val T' = TermSubst.instantiateT instT0 T
    3.18        in (cert (Var ((a, i), T')), cert (Free ((a, T')))) end);
    3.19    in Thm.instantiate (instT, inst) th end;
    3.20  
     4.1 --- a/src/Pure/proofterm.ML	Tue Sep 12 12:12:39 2006 +0200
     4.2 +++ b/src/Pure/proofterm.ML	Tue Sep 12 12:12:46 2006 +0200
     4.3 @@ -421,12 +421,12 @@
     4.4  
     4.5  (**** substitutions ****)
     4.6  
     4.7 -fun del_conflicting_tvars envT T = Term.instantiateT
     4.8 +fun del_conflicting_tvars envT T = TermSubst.instantiateT
     4.9    (map_filter (fn ixnS as (_, S) =>
    4.10       (Type.lookup (envT, ixnS); NONE) handle TYPE _ =>
    4.11          SOME (ixnS, TFree ("'dummy", S))) (typ_tvars T)) T;
    4.12  
    4.13 -fun del_conflicting_vars env t = Term.instantiate
    4.14 +fun del_conflicting_vars env t = TermSubst.instantiate
    4.15    (map_filter (fn ixnS as (_, S) =>
    4.16       (Type.lookup (type_env env, ixnS); NONE) handle TYPE _ =>
    4.17          SOME (ixnS, TFree ("'dummy", S))) (term_tvars t),
    4.18 @@ -665,16 +665,16 @@
    4.19  
    4.20  fun generalize (tfrees, frees) idx =
    4.21    map_proof_terms_option
    4.22 -    (Term.generalize_option (tfrees, frees) idx)
    4.23 -    (Term.generalizeT_option tfrees idx);
    4.24 +    (TermSubst.generalize_option (tfrees, frees) idx)
    4.25 +    (TermSubst.generalizeT_option tfrees idx);
    4.26  
    4.27  
    4.28  (***** instantiation *****)
    4.29  
    4.30  fun instantiate (instT, inst) =
    4.31    map_proof_terms_option
    4.32 -    (Term.instantiate_option (instT, map (apsnd remove_types) inst))
    4.33 -    (Term.instantiateT_option instT);
    4.34 +    (TermSubst.instantiate_option (instT, map (apsnd remove_types) inst))
    4.35 +    (TermSubst.instantiateT_option instT);
    4.36  
    4.37  
    4.38  (***** lifting *****)
     5.1 --- a/src/Pure/variable.ML	Tue Sep 12 12:12:39 2006 +0200
     5.2 +++ b/src/Pure/variable.ML	Tue Sep 12 12:12:46 2006 +0200
     5.3 @@ -322,19 +322,19 @@
     5.4  fun exportT_inst inner outer = #1 (export_inst inner outer);
     5.5  
     5.6  fun exportT_terms inner outer ts =
     5.7 -  map (Term.generalize (exportT_inst (fold declare_type_occs ts inner) outer, [])
     5.8 +  map (TermSubst.generalize (exportT_inst (fold declare_type_occs ts inner) outer, [])
     5.9      (fold (Term.fold_types Term.maxidx_typ) ts ~1 + 1)) ts;
    5.10  
    5.11  fun export_terms inner outer ts =
    5.12 -  map (Term.generalize (export_inst (fold declare_type_occs ts inner) outer)
    5.13 +  map (TermSubst.generalize (export_inst (fold declare_type_occs ts inner) outer)
    5.14      (fold Term.maxidx_term ts ~1 + 1)) ts;
    5.15  
    5.16  fun export_prf inner outer prf =
    5.17    let
    5.18      val insts = export_inst (declare_prf prf inner) outer;
    5.19      val idx = Proofterm.maxidx_proof prf ~1 + 1;
    5.20 -    val gen_term = Term.generalize_option insts idx;
    5.21 -    val gen_typ = Term.generalizeT_option (#1 insts) idx;
    5.22 +    val gen_term = TermSubst.generalize_option insts idx;
    5.23 +    val gen_typ = TermSubst.generalizeT_option (#1 insts) idx;
    5.24    in Proofterm.map_proof_terms_option gen_term gen_typ prf end;
    5.25  
    5.26  fun gen_export inst inner outer ths =
    5.27 @@ -359,18 +359,18 @@
    5.28    let
    5.29      val ren = if is_open then I else Name.internal;
    5.30      val (instT, ctxt') = importT_inst ts ctxt;
    5.31 -    val vars = map (apsnd (Term.instantiateT instT)) (rev (fold Term.add_vars ts []));
    5.32 +    val vars = map (apsnd (TermSubst.instantiateT instT)) (rev (fold Term.add_vars ts []));
    5.33      val (xs, ctxt'') = invent_fixes (map (ren o #1 o #1) vars) ctxt';
    5.34      val inst = vars ~~ map Free (xs ~~ map #2 vars);
    5.35    in ((instT, inst), ctxt'') end;
    5.36  
    5.37  fun importT_terms ts ctxt =
    5.38    let val (instT, ctxt') = importT_inst ts ctxt
    5.39 -  in (map (Term.instantiate (instT, [])) ts, ctxt') end;
    5.40 +  in (map (TermSubst.instantiate (instT, [])) ts, ctxt') end;
    5.41  
    5.42  fun import_terms is_open ts ctxt =
    5.43    let val (inst, ctxt') = import_inst is_open ts ctxt
    5.44 -  in (map (Term.instantiate inst) ts, ctxt') end;
    5.45 +  in (map (TermSubst.instantiate inst) ts, ctxt') end;
    5.46  
    5.47  fun importT ths ctxt =
    5.48    let
    5.49 @@ -472,6 +472,6 @@
    5.50      val occs' = type_occs_of ctxt';
    5.51      val types = Symtab.fold (fn (a, _) => if Symtab.defined occs a then I else cons a) occs' [];
    5.52      val idx = fold (Term.fold_types Term.maxidx_typ) ts ~1 + 1;
    5.53 -  in map (Term.generalize (types, []) idx) ts end;
    5.54 +  in map (TermSubst.generalize (types, []) idx) ts end;
    5.55  
    5.56  end;