# HG changeset patch
# User wenzelm
# Date 1544960804 -3600
# Node ID 2633cf136335fd56217c03b6cab9c2beee12b657
# Parent  f71598c11fae8ba6b3b266e61da0ad6dead70008
tuned -- more compact;

diff -r f71598c11fae -r 2633cf136335 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Sat Dec 15 16:42:18 2018 +0100
+++ b/src/Tools/Haskell/Haskell.thy	Sun Dec 16 12:46:44 2018 +0100
@@ -197,17 +197,19 @@
 module Isabelle.Buffer (T, empty, add, content)
 where
 
-newtype T = Buffer [String]
+import Isabelle.Library
+
+
+newtype T = Buffer [Char]
 
 empty :: T
 empty = Buffer []
 
 add :: String -> T -> T
-add "" buf = buf
-add x (Buffer xs) = Buffer (x : xs)
+add s (Buffer cs) = Buffer (fold (:) s cs)
 
 content :: T -> String
-content (Buffer xs) = concat (reverse xs)
+content (Buffer cs) = reverse cs
 \<close>
 
 generate_file "Isabelle/Properties.hs" = \<open>