src/FOLP/simp.ML
changeset 44121 44adaa6db327
parent 42364 8c674b3b8e44
child 56245 84fc7dfa3cd4
     1.1 --- a/src/FOLP/simp.ML	Wed Aug 10 20:12:36 2011 +0200
     1.2 +++ b/src/FOLP/simp.ML	Wed Aug 10 20:53:43 2011 +0200
     1.3 @@ -155,21 +155,21 @@
     1.4  (*ccs contains the names of the constants possessing congruence rules*)
     1.5  fun add_hidden_vars ccs =
     1.6    let fun add_hvars tm hvars = case tm of
     1.7 -              Abs(_,_,body) => OldTerm.add_term_vars(body,hvars)
     1.8 +              Abs(_,_,body) => Misc_Legacy.add_term_vars(body,hvars)
     1.9              | _$_ => let val (f,args) = strip_comb tm
    1.10                       in case f of
    1.11                              Const(c,T) =>
    1.12                                  if member (op =) ccs c
    1.13                                  then fold_rev add_hvars args hvars
    1.14 -                                else OldTerm.add_term_vars (tm, hvars)
    1.15 -                          | _ => OldTerm.add_term_vars (tm, hvars)
    1.16 +                                else Misc_Legacy.add_term_vars (tm, hvars)
    1.17 +                          | _ => Misc_Legacy.add_term_vars (tm, hvars)
    1.18                       end
    1.19              | _ => hvars;
    1.20    in add_hvars end;
    1.21  
    1.22  fun add_new_asm_vars new_asms =
    1.23      let fun itf (tm, at) vars =
    1.24 -                if at then vars else OldTerm.add_term_vars(tm,vars)
    1.25 +                if at then vars else Misc_Legacy.add_term_vars(tm,vars)
    1.26          fun add_list(tm,al,vars) = let val (_,tml) = strip_comb tm
    1.27                  in if length(tml)=length(al)
    1.28                     then fold_rev itf (tml ~~ al) vars
    1.29 @@ -197,7 +197,7 @@
    1.30      val hvars = add_new_asm_vars new_asms (rhs,hvars)
    1.31      fun it_asms asm hvars =
    1.32          if atomic asm then add_new_asm_vars new_asms (asm,hvars)
    1.33 -        else OldTerm.add_term_frees(asm,hvars)
    1.34 +        else Misc_Legacy.add_term_frees(asm,hvars)
    1.35      val hvars = fold_rev it_asms asms hvars
    1.36      val hvs = map (#1 o dest_Var) hvars
    1.37      val refl1_tac = refl_tac 1
    1.38 @@ -543,7 +543,7 @@
    1.39  fun find_subst sg T =
    1.40  let fun find (thm::thms) =
    1.41          let val (Const(_,cT), va, vb) = dest_red(hd(prems_of thm));
    1.42 -            val [P] = subtract (op =) [va, vb] (OldTerm.add_term_vars (concl_of thm, []));
    1.43 +            val [P] = subtract (op =) [va, vb] (Misc_Legacy.add_term_vars (concl_of thm, []));
    1.44              val eqT::_ = binder_types cT
    1.45          in if Sign.typ_instance sg (T,eqT) then SOME(thm,va,vb,P)
    1.46             else find thms