--- 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