# HG changeset patch
# User wenzelm
# Date 1255641035 -7200
# Node ID 83392f9d303f8f8eaf7b1e9368a22f7d568ab454
# Parent  5d5e123443b3a175f6fcaaf8c01e47c5f15ad179
space_implode;

diff -r 5d5e123443b3 -r 83392f9d303f src/HOL/Import/proof_kernel.ML
--- 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