src/HOL/IMP/Abs_State.thy

--- a/src/HOL/IMP/Abs_State.thy	Thu Sep 13 17:20:44 2012 +0200
+++ b/src/HOL/IMP/Abs_State.thy	Fri Sep 14 10:01:42 2012 +0200
@@ -52,7 +52,7 @@
 definition wt_option where
 "wt opt X = (case opt of None \<Rightarrow> True | Some x \<Rightarrow> wt x X)"
 
-lemma wt_simps[simp]: "wt None X" "wt (Some x) X = wt x X"
+lemma wt_option_simps[simp]: "wt None X" "wt (Some x) X = wt x X"
 by(simp_all add: wt_option_def)
 
 instance ..