src/HOL/Import/replay.ML
changeset 21078 101aefd61aac
parent 19349 36e537f89585
child 23139 aa899bce7c3b
     1.1 --- a/src/HOL/Import/replay.ML	Fri Oct 20 17:07:25 2006 +0200
     1.2 +++ b/src/HOL/Import/replay.ML	Fri Oct 20 17:07:26 2006 +0200
     1.3 @@ -27,12 +27,12 @@
     1.4  	    end
     1.5  	  | rp (PSubst(prfs,ctxt,prf)) thy =
     1.6  	    let
     1.7 -		val (thy',ths) = foldr (fn (p,(thy,ths)) =>
     1.8 +		val (thy',ths) = fold_rev (fn p => fn (thy, ths) =>
     1.9  					   let
    1.10  					       val (thy',th) = rp' p thy
    1.11  					   in
    1.12  					       (thy',th::ths)
    1.13 -					   end) (thy,[]) prfs
    1.14 +					   end) prfs (thy,[])
    1.15  		val (thy'',th) = rp' prf thy'
    1.16  	    in
    1.17  		P.SUBST ths ctxt th thy''