1.1 --- a/src/HOL/ex/FinFunPred.thy	Tue May 29 15:31:58 2012 +0200
     1.2 +++ b/src/HOL/ex/FinFunPred.thy	Tue May 29 16:08:12 2012 +0200
     1.3 @@ -195,7 +195,7 @@
     1.4  
     1.5  lemma iso_finfun_eq [code_unfold]:
     1.6    "A\<^sub>f = B\<^sub>f \<longleftrightarrow> A = B"
     1.7 -by(simp add: expand_finfun_eq)
     1.8 +by(simp only: expand_finfun_eq)
     1.9  
    1.10  lemma iso_finfun_sup [code_unfold]:
    1.11    "sup A\<^sub>f B\<^sub>f = (sup A B)\<^sub>f"