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/Pure/Proof/extraction.ML
changeset 33245 65232054ffd0
parent 33038 8f9594c31de4
child 33317 b4534348b8fd 
--- a/src/Pure/Proof/extraction.ML	Tue Oct 27 22:55:27 2009 +0100
+++ b/src/Pure/Proof/extraction.ML	Tue Oct 27 22:56:14 2009 +0100
@@ -716,8 +716,9 @@
           quote name ^ " has no computational content")
       in (Reconstruct.reconstruct_proof thy prop prf, vs) end;
 
-    val defs = Library.foldl (fn (defs, (prf, vs)) =>
-      fst (extr 0 defs vs [] [] [] prf)) ([], map prep_thm thms);
+    val defs =
+      fold (fn (prf, vs) => fn defs => fst (extr 0 defs vs [] [] [] prf))
+        (map prep_thm thms) [];
 
     fun add_def (s, (vs, ((t, u), (prf, _)))) thy =
       (case Sign.const_type thy (extr_name s vs) of
isabelle