src/Pure/thm.ML
changeset 23178 07ba6b58b3d2
parent 22909 7de3b0ac4189
child 23296 25f28f9c28a3
     1.1 --- a/src/Pure/thm.ML	Thu May 31 23:02:16 2007 +0200
     1.2 +++ b/src/Pure/thm.ML	Thu May 31 23:47:36 2007 +0200
     1.3 @@ -1150,7 +1150,7 @@
     1.4  (* Replace all TFrees not fixed or in the hyps by new TVars *)
     1.5  fun varifyT' fixed (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop, ...}) =
     1.6    let
     1.7 -    val tfrees = foldr add_term_tfrees fixed hyps;
     1.8 +    val tfrees = List.foldr add_term_tfrees fixed hyps;
     1.9      val prop1 = attach_tpairs tpairs prop;
    1.10      val (al, prop2) = Type.varify tfrees prop1;
    1.11      val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
    1.12 @@ -1430,7 +1430,7 @@
    1.13  
    1.14  (*Function to rename bounds/unknowns in the argument, lifted over B*)
    1.15  fun rename_bvars(dpairs, tpairs, B) =
    1.16 -        rename_bvs(foldr Term.match_bvars [] dpairs, dpairs, tpairs, B);
    1.17 +        rename_bvs(List.foldr Term.match_bvars [] dpairs, dpairs, tpairs, B);
    1.18  
    1.19  
    1.20  (*** RESOLUTION ***)