src/Pure/thm.ML
changeset 29272 fb3ccf499df5
parent 29269 5c25a2012975
child 29288 253bcf2a5854
     1.1 --- a/src/Pure/thm.ML	Wed Dec 31 18:53:16 2008 +0100
     1.2 +++ b/src/Pure/thm.ML	Wed Dec 31 18:53:17 2008 +0100
     1.3 @@ -1154,7 +1154,7 @@
     1.4  (* Replace all TFrees not fixed or in the hyps by new TVars *)
     1.5  fun varifyT' fixed (Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
     1.6    let
     1.7 -    val tfrees = List.foldr add_term_tfrees fixed hyps;
     1.8 +    val tfrees = fold Term.add_tfrees hyps fixed;
     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);