diff -r c724a9093ebe -r c9ffdd63dd93 src/HOL/Induct/Term.thy
--- a/src/HOL/Induct/Term.thy	Tue Oct 16 17:56:12 2001 +0200
+++ b/src/HOL/Induct/Term.thy	Tue Oct 16 17:58:13 2001 +0200
@@ -36,7 +36,7 @@
     (subst_term f1 (subst_term f2 t)) \<and>
   (subst_term_list ((subst_term f1) \<circ> f2) ts) =
     (subst_term_list f1 (subst_term_list f2 ts))"
-  apply (induct t and ts rule: term.induct)
+  apply (induct t and ts)
      apply simp_all
   done
 
@@ -50,7 +50,7 @@
 proof -
   case rule_context
   have "P t \<and> list_all P ts"
-    apply (induct t and ts rule: term.induct)
+    apply (induct t and ts)
        apply (rule rule_context)
       apply (rule rule_context)
       apply assumption