src/Tools/Haskell/Haskell.thy

 {-# LANGUAGE InstanceSigs #-}
 
 module Isabelle.Library (
   (|>), (|->), (#>), (#->),
 
-  fold, fold_rev, single, the_single, map_index, get_index, separate,
+  fold, fold_rev, single, the_single, singletonM, map_index, get_index, separate,
 
   StringLike, STRING (..), TEXT (..), BYTES (..),
   show_bytes, show_text,
 
   proper_string, enclose, quote, space_implode, commas, commas_quote, cat_lines,

 single x = [x]
 
 the_single :: [a] -> a
 the_single [x] = x
 the_single _ = undefined
+
+singletonM :: Monad m => ([a] -> m [b]) -> a -> m b
+singletonM f x = the_single <$> f [x]
 
 map_index :: ((Int, a) -> b) -> [a] -> [b]
 map_index f = map_aux 0
   where
     map_aux _ [] = []