Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Import/replay.ML
changeset 15574 b1d1b5bfc464
parent 15570 8d8c70b41bab
child 17322 781abf7011e6 
--- a/src/HOL/Import/replay.ML	Fri Mar 04 11:44:26 2005 +0100
+++ b/src/HOL/Import/replay.ML	Fri Mar 04 15:07:34 2005 +0100
@@ -25,12 +25,12 @@
 	    end
 	  | rp (PSubst(prfs,ctxt,prf)) thy =
 	    let
-		val (thy',ths) = Library.foldr (fn (p,(thy,ths)) =>
+		val (thy',ths) = foldr (fn (p,(thy,ths)) =>
 					   let
 					       val (thy',th) = rp' p thy
 					   in
 					       (thy',th::ths)
-					   end) (prfs,(thy,[]))
+					   end) (thy,[]) prfs
 		val (thy'',th) = rp' prf thy'
 	    in
 		P.SUBST ths ctxt th thy''
isabelle