src/Pure/drule.ML
changeset 23178 07ba6b58b3d2
parent 22939 2afc93a3d8f4
child 23423 b2d64f86d21b
     1.1 --- a/src/Pure/drule.ML	Thu May 31 23:02:16 2007 +0200
     1.2 +++ b/src/Pure/drule.ML	Thu May 31 23:47:36 2007 +0200
     1.3 @@ -401,7 +401,7 @@
     1.4   let val fth = Thm.freezeT th
     1.5       val {prop, tpairs, thy, ...} = rep_thm fth
     1.6   in
     1.7 -   case foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
     1.8 +   case List.foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
     1.9         [] => (fth, fn i => fn x => x)   (*No vars: nothing to do!*)
    1.10       | vars =>
    1.11           let fun newName (Var(ix,_)) = (ix, gensym (string_of_indexname ix))
    1.12 @@ -423,13 +423,13 @@
    1.13   let val fth = Thm.freezeT th
    1.14       val {prop, tpairs, thy, ...} = rep_thm fth
    1.15   in
    1.16 -   case foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
    1.17 +   case List.foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
    1.18         [] => (fth, fn x => x)
    1.19       | vars =>
    1.20           let fun newName (Var(ix,_), (pairs,used)) =
    1.21                     let val v = Name.variant used (string_of_indexname ix)
    1.22                     in  ((ix,v)::pairs, v::used)  end;
    1.23 -             val (alist, _) = foldr newName ([], Library.foldr add_term_names
    1.24 +             val (alist, _) = List.foldr newName ([], Library.foldr add_term_names
    1.25                 (prop :: Thm.terms_of_tpairs tpairs, [])) vars
    1.26               fun mk_inst (Var(v,T)) =
    1.27                   (cterm_of thy (Var(v,T)),
    1.28 @@ -810,7 +810,7 @@
    1.29  in
    1.30  fun cterm_instantiate [] th = th
    1.31    | cterm_instantiate ctpairs0 th =
    1.32 -  let val (thy,tye,_) = foldr add_types (Thm.theory_of_thm th, Vartab.empty, 0) ctpairs0
    1.33 +  let val (thy,tye,_) = List.foldr add_types (Thm.theory_of_thm th, Vartab.empty, 0) ctpairs0
    1.34        fun instT(ct,cu) =
    1.35          let val inst = cterm_of thy o Term.map_types (Envir.norm_type tye) o term_of
    1.36          in (inst ct, inst cu) end