--- a/src/HOL/IMP/Abs_State.thy Tue May 14 21:56:19 2013 +0200
+++ b/src/HOL/IMP/Abs_State.thy Thu May 16 02:13:23 2013 +0200
@@ -156,7 +156,7 @@
by(induction S1 S2 rule: less_eq_option.induct)(simp_all add: mono_gamma_s)
lemma mono_gamma_c: "C1 \<le> C2 \<Longrightarrow> \<gamma>\<^isub>c C1 \<le> \<gamma>\<^isub>c C2"
-by (induction C1 C2 rule: less_eq_acom.induct) (simp_all add:mono_gamma_o)
+by (simp add: less_eq_acom_def mono_gamma_o size_annos anno_map_acom size_annos_same[of C1 C2])
lemma in_gamma_option_iff:
"x : \<gamma>_option r u \<longleftrightarrow> (\<exists>u'. u = Some u' \<and> x : r u')"