src/HOL/Import/replay.ML
changeset 15574 b1d1b5bfc464
parent 15570 8d8c70b41bab
child 17322 781abf7011e6
     1.1 --- a/src/HOL/Import/replay.ML	Fri Mar 04 11:44:26 2005 +0100
     1.2 +++ b/src/HOL/Import/replay.ML	Fri Mar 04 15:07:34 2005 +0100
     1.3 @@ -25,12 +25,12 @@
     1.4  	    end
     1.5  	  | rp (PSubst(prfs,ctxt,prf)) thy =
     1.6  	    let
     1.7 -		val (thy',ths) = Library.foldr (fn (p,(thy,ths)) =>
     1.8 +		val (thy',ths) = foldr (fn (p,(thy,ths)) =>
     1.9  					   let
    1.10  					       val (thy',th) = rp' p thy
    1.11  					   in
    1.12  					       (thy',th::ths)
    1.13 -					   end) (prfs,(thy,[]))
    1.14 +					   end) (thy,[]) prfs
    1.15  		val (thy'',th) = rp' prf thy'
    1.16  	    in
    1.17  		P.SUBST ths ctxt th thy''