src/HOL/Import/replay.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15574 b1d1b5bfc464
     1.1 --- a/src/HOL/Import/replay.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/HOL/Import/replay.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -25,7 +25,7 @@
     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) = Library.foldr (fn (p,(thy,ths)) =>
     1.9  					   let
    1.10  					       val (thy',th) = rp' p thy
    1.11  					   in
    1.12 @@ -319,7 +319,7 @@
    1.13  	    in
    1.14  		fst (replay_proof int_thms thyname thmname prf thy)
    1.15  	    end
    1.16 -	val res_thy = foldl replay_fact (thy,thmnames)
    1.17 +	val res_thy = Library.foldl replay_fact (thy,thmnames)
    1.18      in
    1.19  	res_thy
    1.20      end