--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy Wed Feb 12 14:32:45 2014 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy Wed Feb 12 16:35:58 2014 +0100
@@ -196,7 +196,7 @@
lemma strip_pfp_wn:
"\<lbrakk> \<forall>c. strip(f c) = strip c; pfp_wn f c = Some c' \<rbrakk> \<Longrightarrow> strip c' = c"
apply(auto simp add: pfp_wn_def iter_narrow_def split: option.splits)
-by (metis (no_types) strip_map2_acom strip_while strip_bot_acom strip_iter_widen)
+by (metis (mono_tags) strip_map2_acom strip_while strip_bot_acom strip_iter_widen)
locale Abs_Int2 = Abs_Int1_mono
where \<gamma>=\<gamma> for \<gamma> :: "'av::{WN,L_top_bot} \<Rightarrow> val set"