src/Tools/Haskell/Haskell.thy

     (\infos ->
       case lookup_info infos id of
         Nothing -> (infos, ())
         Just info -> (Map.insert id (f info) infos, ()))
 
+delete_info :: ThreadId -> IO ()
+delete_info id =
+  atomicModifyIORef' global_state (\infos -> (Map.delete id infos, ()))
+
 
 {- thread properties -}
 
 my_info :: IO Info
 my_info = do

       Thread.forkIO
         (Exception.try
           (do
             id <- Concurrent.myThreadId
             atomicModifyIORef' global_state (init_info id uuid)
-            restore body) >>= finally))
+            restore body)
+         >>= (\res -> do id <- Concurrent.myThreadId; delete_info id; finally res)))
   return (id, uuid, result)
 
 fork :: IO a -> IO (Fork a)
 fork body = fork_finally body Thread.result
 \<close>