1.1 --- a/src/ZF/Induct/Term.thy	Tue Mar 13 14:17:42 2012 +0100
     1.2 +++ b/src/ZF/Induct/Term.thy	Tue Mar 13 14:44:16 2012 +0100
     1.3 @@ -138,8 +138,7 @@
     1.4    apply (subst term_rec)
     1.5     apply (assumption | rule a)+
     1.6    apply (erule list.induct)
     1.7 -   apply (simp add: term_rec)
     1.8 -  apply (auto simp add: term_rec)
     1.9 +   apply auto
    1.10    done
    1.11  
    1.12  lemma def_term_rec: