src/HOL/Imperative_HOL/ex/Linked_Lists.thy

   "traverse (Node x r) = do tl \<leftarrow> Ref.lookup r;
                             xs \<leftarrow> traverse tl;
                             return (x#xs)
                          done"
 unfolding traverse_def
-by (auto simp: traverse_def monad_simp MREC_rule)
+by (auto simp: traverse_def MREC_rule)
 
 
 section {* Proving correctness with relational abstraction *}
 
 subsection {* Definition of list_of, list_of', refs_of and refs_of' *}

           rev' (p, next)
         done)
   done"
   unfolding rev'_def MREC_rule[of _ _ "(q, p)"] unfolding rev'_def[symmetric]
 thm arg_cong2
-  by (auto simp add: monad_simp expand_fun_eq intro: arg_cong2[where f = "op \<guillemotright>="] split: node.split)
+  by (auto simp add: expand_fun_eq intro: arg_cong2[where f = "op \<guillemotright>="] split: node.split)
 
 fun rev :: "('a:: heap) node \<Rightarrow> 'a node Heap" 
 where
   "rev Empty = return Empty"
 | "rev (Node x n) = (do q \<leftarrow> Ref.new Empty; p \<leftarrow> Ref.new (Node x n); v \<leftarrow> rev' (q, p); !v done)"