src/HOL/Import/replay.ML
changeset 21078 101aefd61aac
parent 19349 36e537f89585
child 23139 aa899bce7c3b
--- a/src/HOL/Import/replay.ML	Fri Oct 20 17:07:25 2006 +0200
+++ b/src/HOL/Import/replay.ML	Fri Oct 20 17:07:26 2006 +0200
@@ -27,12 +27,12 @@
 	    end
 	  | rp (PSubst(prfs,ctxt,prf)) thy =
 	    let
-		val (thy',ths) = foldr (fn (p,(thy,ths)) =>
+		val (thy',ths) = fold_rev (fn p => fn (thy, ths) =>
 					   let
 					       val (thy',th) = rp' p thy
 					   in
 					       (thy',th::ths)
-					   end) (thy,[]) prfs
+					   end) prfs (thy,[])
 		val (thy'',th) = rp' prf thy'
 	    in
 		P.SUBST ths ctxt th thy''