[isabelle] A fast implementation of concat for strings?

Dear list,

I recently learned that the Isabelle pretty printer for large datatype
constructs can be quite slow.

Andreas explained that not printing (only evaluating) the result
helps, for example
value [code] "let x = expression in ()"

To get some debug output, I started writing custom toString functions
in HOL to print some complicated datatypes. This was sufficiently

value [code] "let x = expression in something_toString x"

However, as datatypes get more complex, my toString functions also get
slow. My question: Is there a fast implementation of concat for

Currently, concat is a huge bottleneck:

value[code] "replicate 1000

value[code] "concat (replicate 1000


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.