src/Pure/thm.ML
changeset 31977 e03059ae2d82
parent 31947 7daee3bed3af
child 32027 9dd548810ed1
     1.1 --- a/src/Pure/thm.ML	Thu Jul 09 22:36:11 2009 +0200
     1.2 +++ b/src/Pure/thm.ML	Thu Jul 09 22:48:12 2009 +0200
     1.3 @@ -995,7 +995,7 @@
     1.4          val _ = exists bad_term hyps andalso
     1.5            raise THM ("generalize: variable free in assumptions", 0, [th]);
     1.6  
     1.7 -        val gen = TermSubst.generalize (tfrees, frees) idx;
     1.8 +        val gen = Term_Subst.generalize (tfrees, frees) idx;
     1.9          val prop' = gen prop;
    1.10          val tpairs' = map (pairself gen) tpairs;
    1.11          val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop');
    1.12 @@ -1066,7 +1066,7 @@
    1.13          val Thm (der, {thy_ref, hyps, shyps, tpairs, prop, ...}) = th;
    1.14          val (inst', (instT', (thy_ref', shyps'))) =
    1.15            (thy_ref, shyps) |> fold_map add_inst inst ||> fold_map add_instT instT;
    1.16 -        val subst = TermSubst.instantiate_maxidx (instT', inst');
    1.17 +        val subst = Term_Subst.instantiate_maxidx (instT', inst');
    1.18          val (prop', maxidx1) = subst prop ~1;
    1.19          val (tpairs', maxidx') =
    1.20            fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1;
    1.21 @@ -1088,8 +1088,8 @@
    1.22          val Cterm {thy_ref, t, T, sorts, ...} = ct;
    1.23          val (inst', (instT', (thy_ref', sorts'))) =
    1.24            (thy_ref, sorts) |> fold_map add_inst inst ||> fold_map add_instT instT;
    1.25 -        val subst = TermSubst.instantiate_maxidx (instT', inst');
    1.26 -        val substT = TermSubst.instantiateT_maxidx instT';
    1.27 +        val subst = Term_Subst.instantiate_maxidx (instT', inst');
    1.28 +        val substT = Term_Subst.instantiateT_maxidx instT';
    1.29          val (t', maxidx1) = subst t ~1;
    1.30          val (T', maxidx') = substT T maxidx1;
    1.31        in Cterm {thy_ref = thy_ref', t = t', T = T', sorts = sorts', maxidx = maxidx'} end