tuned -- more compact;
authorwenzelm
Sun, 16 Dec 2018 12:46:44 +0100
changeset 69474 2633cf136335
parent 69473 f71598c11fae
child 69475 b3628ee55f28
tuned -- more compact;
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>