src/Tools/Haskell/Haskell.thy

 {-# LANGUAGE InstanceSigs #-}
 
 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,
 
   proper_string, enclose, quote, space_implode, commas, commas_quote, cat_lines,

 fold_rev _ [] y = y
 fold_rev f (x : xs) y = f x (fold_rev f xs y)
 
 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
     map_aux _ [] = []