diff -r 1d26f1a49480 -r dc962d4248ca src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Sat Jul 31 12:24:13 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Sat Jul 31 12:48:01 2021 +0200
@@ -178,6 +178,8 @@
 -}
 
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
 
 module Isabelle.Library (
   (|>), (|->), (#>), (#->),
@@ -186,13 +188,19 @@
 
   fold, fold_rev, single, map_index, get_index, separate,
 
+  StringLike, STRING (..), TEXT (..), BYTES (..),
+
   proper_string, quote, space_implode, commas, commas_quote, cat_lines,
   space_explode, split_lines, trim_line, clean_name)
 where
 
+import qualified Data.Text as Text
+import Data.Text (Text)
 import Data.String (IsString)
 import qualified Data.List.Split as Split
 import qualified Isabelle.Symbol as Symbol
+import Isabelle.Bytes (Bytes)
+import qualified Isabelle.UTF8 as UTF8
 
 
 {- functions -}
@@ -250,26 +258,49 @@
         Just y -> Just (i, y)
 
 separate :: a -> [a] -> [a]
-separate s (x : xs @ (_ : _)) = x : s : separate s xs
+separate s (x : (xs @ (_ : _))) = x : s : separate s xs
 separate _ xs = xs;
 
 
+{- string-like interfaces -}
+
+class (IsString a, Monoid a, Eq a, Ord a) => StringLike a
+instance StringLike String
+instance StringLike Text
+instance StringLike Bytes
+
+class StringLike a => STRING a where make_string :: a -> String
+instance STRING String where make_string = id
+instance STRING Text where make_string = Text.unpack
+instance STRING Bytes where make_string = UTF8.decode
+
+class StringLike a => TEXT a where make_text :: a -> Text
+instance TEXT String where make_text = Text.pack
+instance TEXT Text where make_text = id
+instance TEXT Bytes where make_text = UTF8.decode
+
+class StringLike a => BYTES a where make_bytes :: a -> Bytes
+instance BYTES String where make_bytes = UTF8.encode
+instance BYTES Text where make_bytes = UTF8.encode
+instance BYTES Bytes where make_bytes = id
+
+
 {- strings -}
 
-proper_string :: (IsString a, Eq a) => a -> Maybe a
+proper_string :: StringLike a => a -> Maybe a
 proper_string s = if s == "" then Nothing else Just s
 
-quote :: (IsString a, Semigroup a) => a -> a
+quote :: StringLike a => a -> a
 quote s = "\"" <> s <> "\""
 
-space_implode :: (IsString a, Monoid a) => a -> [a] -> a
+space_implode :: StringLike a => a -> [a] -> a
 space_implode s = mconcat . separate s
 
-commas, commas_quote :: (IsString a, Monoid a) => [a] -> a
+commas, commas_quote :: StringLike a => [a] -> a
 commas = space_implode ", "
 commas_quote = commas . map quote
 
-cat_lines :: (IsString a, Monoid a) => [a] -> a
+cat_lines :: StringLike a => [a] -> a
 cat_lines = space_implode "\n"