src/HOL/Imperative_HOL/Mrec.thy
changeset 37787 30dc3abf4a58
parent 37772 026ed2fc15d4
child 37792 ba0bc31b90d7
--- a/src/HOL/Imperative_HOL/Mrec.thy	Tue Jul 13 02:29:05 2010 +0200
+++ b/src/HOL/Imperative_HOL/Mrec.thy	Tue Jul 13 11:38:03 2010 +0200
@@ -76,7 +76,7 @@
   apply simp
   apply (rule ext)
   apply (unfold mrec_rule[of x])
-  by (auto split: option.splits prod.splits sum.splits)
+  by (auto simp add: execute_simps split: option.splits prod.splits sum.splits)
 
 lemma MREC_pinduct:
   assumes "execute (MREC x) h = Some (r, h')"