--- a/src/HOL/SMT.thy Thu May 27 17:09:37 2010 +0200 +++ b/src/HOL/SMT.thy Thu May 27 18:16:54 2010 +0200 @@ -68,7 +68,7 @@ *} lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other - fun_upd_upd + fun_upd_upd fun_app_def