diff -r 10455384a3e5 -r 92f08f3d77bd src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Thu Aug 26 16:24:48 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Thu Aug 26 22:15:55 2021 +0200
@@ -222,7 +222,7 @@
 module Isabelle.Library (
   (|>), (|->), (#>), (#->),
 
-  fold, fold_rev, single, map_index, get_index, separate,
+  fold, fold_rev, single, the_single, map_index, get_index, separate,
 
   StringLike, STRING (..), TEXT (..), BYTES (..),
   show_bytes, show_text,
@@ -270,6 +270,10 @@
 single :: a -> [a]
 single x = [x]
 
+the_single :: [a] -> a
+the_single [x] = x
+the_single _ = undefined
+
 map_index :: ((Int, a) -> b) -> [a] -> [b]
 map_index f = map_aux 0
   where