--- a/src/HOL/Library/AList.thy Wed Dec 14 15:56:29 2011 +0100
+++ b/src/HOL/Library/AList.thy Wed Dec 14 15:56:31 2011 +0100
@@ -274,7 +274,7 @@
"map_of (update x y (restrict D al)) = map_of (update x y (restrict (D-{x}) al))"
by (simp add: update_conv' restr_conv') (rule fun_upd_restrict)
-lemma upate_restr_conv [simp]:
+lemma update_restr_conv [simp]:
"x \<in> D \<Longrightarrow>
map_of (update x y (restrict D al)) = map_of (update x y (restrict (D-{x}) al))"
by (simp add: update_conv' restr_conv')