renamed structure TermSubst to Term_Subst;
authorwenzelm
Thu Jul 09 22:48:12 2009 +0200 (2009-07-09)
changeset 31977e03059ae2d82
parent 31976 17414e2736f4
child 31980 c7c1d545007e
renamed structure TermSubst to Term_Subst;
src/Pure/Isar/expression.ML
src/Pure/Isar/rule_insts.ML
src/Pure/Isar/theory_target.ML
src/Pure/consts.ML
src/Pure/drule.ML
src/Pure/more_thm.ML
src/Pure/proofterm.ML
src/Pure/term_subst.ML
src/Pure/thm.ML
src/Pure/type_infer.ML
src/Pure/variable.ML
src/Tools/Code/code_preproc.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Thu Jul 09 22:36:11 2009 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Thu Jul 09 22:48:12 2009 +0200
     1.3 @@ -492,7 +492,7 @@
     1.4  
     1.5      val export = Variable.export_morphism goal_ctxt context;
     1.6      val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
     1.7 -    val exp_term = TermSubst.zero_var_indexes o Morphism.term export;
     1.8 +    val exp_term = Term_Subst.zero_var_indexes o Morphism.term export;
     1.9      val exp_typ = Logic.type_map exp_term;
    1.10      val export' = Morphism.morphism {binding = I, typ = exp_typ, term = exp_term, fact = exp_fact};
    1.11    in ((propss, deps, export'), goal_ctxt) end;
     2.1 --- a/src/Pure/Isar/rule_insts.ML	Thu Jul 09 22:36:11 2009 +0200
     2.2 +++ b/src/Pure/Isar/rule_insts.ML	Thu Jul 09 22:48:12 2009 +0200
     2.3 @@ -58,7 +58,7 @@
     2.4    end;
     2.5  
     2.6  fun instantiate inst =
     2.7 -  TermSubst.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #>
     2.8 +  Term_Subst.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #>
     2.9    Envir.beta_norm;
    2.10  
    2.11  fun make_instT f v =
    2.12 @@ -124,7 +124,7 @@
    2.13        end;
    2.14  
    2.15      val type_insts1 = map readT type_insts;
    2.16 -    val instT1 = TermSubst.instantiateT type_insts1;
    2.17 +    val instT1 = Term_Subst.instantiateT type_insts1;
    2.18      val vars1 = map (apsnd instT1) vars;
    2.19  
    2.20  
     3.1 --- a/src/Pure/Isar/theory_target.ML	Thu Jul 09 22:36:11 2009 +0200
     3.2 +++ b/src/Pure/Isar/theory_target.ML	Thu Jul 09 22:48:12 2009 +0200
     3.3 @@ -130,7 +130,7 @@
     3.4      val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees);
     3.5      val inst = filter (is_Var o fst) (vars ~~ frees);
     3.6      val cinstT = map (pairself certT o apfst TVar) instT;
     3.7 -    val cinst = map (pairself (cert o Term.map_types (TermSubst.instantiateT instT))) inst;
     3.8 +    val cinst = map (pairself (cert o Term.map_types (Term_Subst.instantiateT instT))) inst;
     3.9      val result' = Thm.instantiate (cinstT, cinst) result;
    3.10  
    3.11      (*import assumes/defines*)
     4.1 --- a/src/Pure/consts.ML	Thu Jul 09 22:36:11 2009 +0200
     4.2 +++ b/src/Pure/consts.ML	Thu Jul 09 22:48:12 2009 +0200
     4.3 @@ -215,7 +215,7 @@
     4.4      val vars = map Term.dest_TVar (typargs consts (c, declT));
     4.5      val inst = vars ~~ Ts handle UnequalLengths =>
     4.6        raise TYPE ("Consts.instance", Ts, [Const (c, dummyT)]);
     4.7 -  in declT |> TermSubst.instantiateT inst end;
     4.8 +  in declT |> Term_Subst.instantiateT inst end;
     4.9  
    4.10  
    4.11  
     5.1 --- a/src/Pure/drule.ML	Thu Jul 09 22:36:11 2009 +0200
     5.2 +++ b/src/Pure/drule.ML	Thu Jul 09 22:48:12 2009 +0200
     5.3 @@ -278,7 +278,7 @@
     5.4        let
     5.5          val thy = Theory.merge_list (map Thm.theory_of_thm ths);
     5.6          val certT = Thm.ctyp_of thy and cert = Thm.cterm_of thy;
     5.7 -        val (instT, inst) = TermSubst.zero_var_indexes_inst (map Thm.full_prop_of ths);
     5.8 +        val (instT, inst) = Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths);
     5.9          val cinstT = map (fn (v, T) => (certT (TVar v), certT T)) instT;
    5.10          val cinst = map (fn (v, t) => (cert (Var v), cert t)) inst;
    5.11        in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate (cinstT, cinst)) ths end;
     6.1 --- a/src/Pure/more_thm.ML	Thu Jul 09 22:36:11 2009 +0200
     6.2 +++ b/src/Pure/more_thm.ML	Thu Jul 09 22:48:12 2009 +0200
     6.3 @@ -274,7 +274,7 @@
     6.4      val instT0 = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S)));
     6.5      val instT = map (fn (v, T) => (certT (TVar v), certT T)) instT0;
     6.6      val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) =>
     6.7 -      let val T' = TermSubst.instantiateT instT0 T
     6.8 +      let val T' = Term_Subst.instantiateT instT0 T
     6.9        in (cert (Var ((a, i), T')), cert (Free ((a, T')))) end);
    6.10    in Thm.instantiate (instT, inst) th end;
    6.11  
     7.1 --- a/src/Pure/proofterm.ML	Thu Jul 09 22:36:11 2009 +0200
     7.2 +++ b/src/Pure/proofterm.ML	Thu Jul 09 22:48:12 2009 +0200
     7.3 @@ -441,12 +441,12 @@
     7.4  
     7.5  (**** substitutions ****)
     7.6  
     7.7 -fun del_conflicting_tvars envT T = TermSubst.instantiateT
     7.8 +fun del_conflicting_tvars envT T = Term_Subst.instantiateT
     7.9    (map_filter (fn ixnS as (_, S) =>
    7.10       (Type.lookup envT ixnS; NONE) handle TYPE _ =>
    7.11          SOME (ixnS, TFree ("'dummy", S))) (OldTerm.typ_tvars T)) T;
    7.12  
    7.13 -fun del_conflicting_vars env t = TermSubst.instantiate
    7.14 +fun del_conflicting_vars env t = Term_Subst.instantiate
    7.15    (map_filter (fn ixnS as (_, S) =>
    7.16       (Type.lookup (type_env env) ixnS; NONE) handle TYPE _ =>
    7.17          SOME (ixnS, TFree ("'dummy", S))) (OldTerm.term_tvars t),
    7.18 @@ -689,16 +689,16 @@
    7.19  
    7.20  fun generalize (tfrees, frees) idx =
    7.21    map_proof_terms_option
    7.22 -    (TermSubst.generalize_option (tfrees, frees) idx)
    7.23 -    (TermSubst.generalizeT_option tfrees idx);
    7.24 +    (Term_Subst.generalize_option (tfrees, frees) idx)
    7.25 +    (Term_Subst.generalizeT_option tfrees idx);
    7.26  
    7.27  
    7.28  (***** instantiation *****)
    7.29  
    7.30  fun instantiate (instT, inst) =
    7.31    map_proof_terms_option
    7.32 -    (TermSubst.instantiate_option (instT, map (apsnd remove_types) inst))
    7.33 -    (TermSubst.instantiateT_option instT);
    7.34 +    (Term_Subst.instantiate_option (instT, map (apsnd remove_types) inst))
    7.35 +    (Term_Subst.instantiateT_option instT);
    7.36  
    7.37  
    7.38  (***** lifting *****)
     8.1 --- a/src/Pure/term_subst.ML	Thu Jul 09 22:36:11 2009 +0200
     8.2 +++ b/src/Pure/term_subst.ML	Thu Jul 09 22:48:12 2009 +0200
     8.3 @@ -25,7 +25,7 @@
     8.4      ((indexname * sort) * typ) list * ((indexname * typ) * term) list
     8.5  end;
     8.6  
     8.7 -structure TermSubst: TERM_SUBST =
     8.8 +structure Term_Subst: TERM_SUBST =
     8.9  struct
    8.10  
    8.11  (* generalization of fixed variables *)
     9.1 --- a/src/Pure/thm.ML	Thu Jul 09 22:36:11 2009 +0200
     9.2 +++ b/src/Pure/thm.ML	Thu Jul 09 22:48:12 2009 +0200
     9.3 @@ -995,7 +995,7 @@
     9.4          val _ = exists bad_term hyps andalso
     9.5            raise THM ("generalize: variable free in assumptions", 0, [th]);
     9.6  
     9.7 -        val gen = TermSubst.generalize (tfrees, frees) idx;
     9.8 +        val gen = Term_Subst.generalize (tfrees, frees) idx;
     9.9          val prop' = gen prop;
    9.10          val tpairs' = map (pairself gen) tpairs;
    9.11          val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop');
    9.12 @@ -1066,7 +1066,7 @@
    9.13          val Thm (der, {thy_ref, hyps, shyps, tpairs, prop, ...}) = th;
    9.14          val (inst', (instT', (thy_ref', shyps'))) =
    9.15            (thy_ref, shyps) |> fold_map add_inst inst ||> fold_map add_instT instT;
    9.16 -        val subst = TermSubst.instantiate_maxidx (instT', inst');
    9.17 +        val subst = Term_Subst.instantiate_maxidx (instT', inst');
    9.18          val (prop', maxidx1) = subst prop ~1;
    9.19          val (tpairs', maxidx') =
    9.20            fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1;
    9.21 @@ -1088,8 +1088,8 @@
    9.22          val Cterm {thy_ref, t, T, sorts, ...} = ct;
    9.23          val (inst', (instT', (thy_ref', sorts'))) =
    9.24            (thy_ref, sorts) |> fold_map add_inst inst ||> fold_map add_instT instT;
    9.25 -        val subst = TermSubst.instantiate_maxidx (instT', inst');
    9.26 -        val substT = TermSubst.instantiateT_maxidx instT';
    9.27 +        val subst = Term_Subst.instantiate_maxidx (instT', inst');
    9.28 +        val substT = Term_Subst.instantiateT_maxidx instT';
    9.29          val (t', maxidx1) = subst t ~1;
    9.30          val (T', maxidx') = substT T maxidx1;
    9.31        in Cterm {thy_ref = thy_ref', t = t', T = T', sorts = sorts', maxidx = maxidx'} end
    10.1 --- a/src/Pure/type_infer.ML	Thu Jul 09 22:36:11 2009 +0200
    10.2 +++ b/src/Pure/type_infer.ML	Thu Jul 09 22:48:12 2009 +0200
    10.3 @@ -64,7 +64,7 @@
    10.4        else (inst, used);
    10.5      val name_context' = (fold o fold_types) Term.declare_typ_names ts name_context;
    10.6      val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], name_context');
    10.7 -  in (map o map_types) (TermSubst.instantiateT inst) ts end;
    10.8 +  in (map o map_types) (Term_Subst.instantiateT inst) ts end;
    10.9  
   10.10  
   10.11  
    11.1 --- a/src/Pure/variable.ML	Thu Jul 09 22:36:11 2009 +0200
    11.2 +++ b/src/Pure/variable.ML	Thu Jul 09 22:48:12 2009 +0200
    11.3 @@ -360,14 +360,14 @@
    11.4  fun exportT_terms inner outer =
    11.5    let val mk_tfrees = exportT_inst inner outer in
    11.6      fn ts => ts |> map
    11.7 -      (TermSubst.generalize (mk_tfrees ts, [])
    11.8 +      (Term_Subst.generalize (mk_tfrees ts, [])
    11.9          (fold (Term.fold_types Term.maxidx_typ) ts ~1 + 1))
   11.10    end;
   11.11  
   11.12  fun export_terms inner outer =
   11.13    let val (mk_tfrees, tfrees) = export_inst inner outer in
   11.14      fn ts => ts |> map
   11.15 -      (TermSubst.generalize (mk_tfrees ts, tfrees)
   11.16 +      (Term_Subst.generalize (mk_tfrees ts, tfrees)
   11.17          (fold Term.maxidx_term ts ~1 + 1))
   11.18    end;
   11.19  
   11.20 @@ -376,8 +376,8 @@
   11.21      val (mk_tfrees, frees) = export_inst (declare_prf prf inner) outer;
   11.22      val tfrees = mk_tfrees [];
   11.23      val idx = Proofterm.maxidx_proof prf ~1 + 1;
   11.24 -    val gen_term = TermSubst.generalize_option (tfrees, frees) idx;
   11.25 -    val gen_typ = TermSubst.generalizeT_option tfrees idx;
   11.26 +    val gen_term = Term_Subst.generalize_option (tfrees, frees) idx;
   11.27 +    val gen_typ = Term_Subst.generalizeT_option tfrees idx;
   11.28    in Proofterm.map_proof_terms_option gen_term gen_typ prf end;
   11.29  
   11.30  
   11.31 @@ -411,18 +411,18 @@
   11.32    let
   11.33      val ren = Name.clean #> (if is_open then I else Name.internal);
   11.34      val (instT, ctxt') = importT_inst ts ctxt;
   11.35 -    val vars = map (apsnd (TermSubst.instantiateT instT)) (rev (fold Term.add_vars ts []));
   11.36 +    val vars = map (apsnd (Term_Subst.instantiateT instT)) (rev (fold Term.add_vars ts []));
   11.37      val (xs, ctxt'') = variant_fixes (map (ren o #1 o #1) vars) ctxt';
   11.38      val inst = vars ~~ map Free (xs ~~ map #2 vars);
   11.39    in ((instT, inst), ctxt'') end;
   11.40  
   11.41  fun importT_terms ts ctxt =
   11.42    let val (instT, ctxt') = importT_inst ts ctxt
   11.43 -  in (map (TermSubst.instantiate (instT, [])) ts, ctxt') end;
   11.44 +  in (map (Term_Subst.instantiate (instT, [])) ts, ctxt') end;
   11.45  
   11.46  fun import_terms is_open ts ctxt =
   11.47    let val (inst, ctxt') = import_inst is_open ts ctxt
   11.48 -  in (map (TermSubst.instantiate inst) ts, ctxt') end;
   11.49 +  in (map (Term_Subst.instantiate inst) ts, ctxt') end;
   11.50  
   11.51  fun importT ths ctxt =
   11.52    let
   11.53 @@ -527,9 +527,9 @@
   11.54      val idx = maxidx_of ctxt' + 1;
   11.55      val Ts' = (fold o fold_types o fold_atyps)
   11.56        (fn T as TFree _ =>
   11.57 -          (case TermSubst.generalizeT types idx T of TVar v => insert (op =) v | _ => I)
   11.58 +          (case Term_Subst.generalizeT types idx T of TVar v => insert (op =) v | _ => I)
   11.59          | _ => I) ts [];
   11.60 -    val ts' = map (TermSubst.generalize (types, []) idx) ts;
   11.61 +    val ts' = map (Term_Subst.generalize (types, []) idx) ts;
   11.62    in (rev Ts', ts') end;
   11.63  
   11.64  fun polymorphic ctxt ts = snd (polymorphic_types ctxt ts);
    12.1 --- a/src/Tools/Code/code_preproc.ML	Thu Jul 09 22:36:11 2009 +0200
    12.2 +++ b/src/Tools/Code/code_preproc.ML	Thu Jul 09 22:48:12 2009 +0200
    12.3 @@ -224,7 +224,7 @@
    12.4  
    12.5  fun default_typscheme_of thy c =
    12.6    let
    12.7 -    val ty = (snd o dest_Const o TermSubst.zero_var_indexes o curry Const c
    12.8 +    val ty = (snd o dest_Const o Term_Subst.zero_var_indexes o curry Const c
    12.9        o Type.strip_sorts o Sign.the_const_type thy) c;
   12.10    in case AxClass.class_of_param thy c
   12.11     of SOME class => ([(Name.aT, [class])], ty)