diff -r adda1dc18bb8 -r bc883b390d91 src/HOL/Tools/induct_method.ML
--- a/src/HOL/Tools/induct_method.ML	Sat Sep 02 21:48:10 2000 +0200
+++ b/src/HOL/Tools/induct_method.ML	Sat Sep 02 21:49:51 2000 +0200
@@ -434,18 +434,15 @@
 val term_dummy = Scan.unless (Scan.lift kind)
   (Scan.lift (Args.$$$ "_") >> K None || Args.local_term >> Some);
 
-fun mode name =
-  Scan.lift (Scan.optional (Args.parens (Args.$$$ name) >> K true) false);
-
 val instss = Args.and_list (Scan.repeat1 term_dummy);
 
 in
 
 val cases_args = Method.syntax
-  (mode simplifiedN -- mode openN -- (instss -- Scan.option cases_rule));
+  (Args.mode simplifiedN -- Args.mode openN -- (instss -- Scan.option cases_rule));
 
 val induct_args = Method.syntax
-  (mode strippedN -- mode openN -- (instss -- Scan.option induct_rule));
+  (Args.mode strippedN -- Args.mode openN -- (instss -- Scan.option induct_rule));
 
 end;