1.1 --- a/src/HOL/IMP/Compiler.thy	Tue May 11 14:00:02 2004 +0200
     1.2 +++ b/src/HOL/IMP/Compiler.thy	Tue May 11 20:11:08 2004 +0200
     1.3 @@ -86,7 +86,7 @@
     1.4  lemma [simp]:
     1.5   "\<And>m n. closed m n (C1@C2) =
     1.6           (closed m (n+size C2) C1 \<and> closed (m+size C1) n C2)"
     1.7 -by(induct C1, simp, simp add:plus_ac0)
     1.8 +by(induct C1, simp, simp add:add_ac)
     1.9  
    1.10  theorem [simp]: "\<And>m n. closed m n (compile c)"
    1.11  by(induct c, simp_all add:backws_def forws_def)