src/HOL/Imperative_HOL/Mrec.thy

           (case mrec s h' of
              Some (z, h'') \<Rightarrow> execute (g x s z) h''
            | None \<Rightarrow> None)
    | None \<Rightarrow> None
    )"
-apply (cases "mrec_dom (x,h)", simp)
+apply (cases "mrec_dom (x,h)", simp add: mrec.psimps)
 apply (frule mrec_default)
 apply (frule mrec_di_reverse, simp)
 by (auto split: sum.split option.split simp: mrec_default)
 
 definition

       note Inl' = this
       show ?thesis
       proof (cases a)
         case (Inl aa)
         from this Inl' 1(1) exec_f mrec non_rec_case show ?thesis
-          by auto
+          by (auto simp: mrec.psimps)
       next
         case (Inr b)
         note Inr' = this
         show ?thesis
         proof (cases "mrec b h1")

           moreover note mrec mrec_rec exec_f Inl' Inr' 1(1) 1(3)
           ultimately show ?thesis
             apply auto
             apply (rule rec_case)
             apply auto
-            unfolding MREC_def by auto
+            unfolding MREC_def by (auto simp: mrec.psimps)
         next
           case None
-          from this 1(1) exec_f mrec Inr' 1(3) show ?thesis by auto
+          from this 1(1) exec_f mrec Inr' 1(3) show ?thesis by (auto simp: mrec.psimps)
         qed
       qed
     next
       case None
-      from this 1(1) mrec 1(3) show ?thesis by simp
+      from this 1(1) mrec 1(3) show ?thesis by (simp add: mrec.psimps)
     qed
   qed
   from this h'_r show ?thesis by simp
 qed