space_implode;
authorwenzelm
Thu Oct 15 23:10:35 2009 +0200 (2009-10-15)
changeset 3295183392f9d303f
parent 32950 5d5e123443b3
child 32952 aeb1e44fbc19
space_implode;
src/HOL/Import/proof_kernel.ML
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Thu Oct 15 21:28:39 2009 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu Oct 15 23:10:35 2009 +0200
     1.3 @@ -1909,7 +1909,7 @@
     1.4          (thy,res)
     1.5      end
     1.6  
     1.7 -val spaces = String.concat o separate " "
     1.8 +val spaces = space_implode " "
     1.9  
    1.10  fun new_definition thyname constname rhs thy =
    1.11      let