Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
space_implode;
authorwenzelm
Thu, 15 Oct 2009 23:10:35 +0200
changeset 32951 83392f9d303f
parent 32950 5d5e123443b3
child 32952 aeb1e44fbc19
space_implode;
src/HOL/Import/proof_kernel.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Import/proof_kernel.ML	Thu Oct 15 21:28:39 2009 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Thu Oct 15 23:10:35 2009 +0200
@@ -1909,7 +1909,7 @@
         (thy,res)
     end
 
-val spaces = String.concat o separate " "
+val spaces = space_implode " "
 
 fun new_definition thyname constname rhs thy =
     let
isabelle