src/ZF/Induct/Tree_Forest.thy

 datatype "tree(A)" = Tcons ("a \<in> A", "f \<in> forest(A)")
   and "forest(A)" = Fnil | Fcons ("t \<in> tree(A)", "f \<in> forest(A)")
 
 (* FIXME *)
 lemmas tree'induct =
-    tree_forest.mutual_induct [THEN conjunct1, THEN spec, THEN [2] rev_mp, of concl: _ t, standard, consumes 1]
+    tree_forest.mutual_induct [THEN conjunct1, THEN spec, THEN [2] rev_mp, of concl: _ t, consumes 1]
   and forest'induct =
-    tree_forest.mutual_induct [THEN conjunct2, THEN spec, THEN [2] rev_mp, of concl: _ f, standard, consumes 1]
+    tree_forest.mutual_induct [THEN conjunct2, THEN spec, THEN [2] rev_mp, of concl: _ f, consumes 1]
+  for t
 
 declare tree_forest.intros [simp, TC]
 
 lemma tree_def: "tree(A) == Part(tree_forest(A), Inl)"
   by (simp only: tree_forest.defs)