diff -r f5417836dbea -r 01594f816e3a src/Tools/induct_tacs.ML --- a/src/Tools/induct_tacs.ML Mon May 17 15:11:25 2010 +0200 +++ b/src/Tools/induct_tacs.ML Mon May 17 23:54:15 2010 +0200 @@ -116,8 +116,7 @@ val opt_rules = Scan.option (rule_spec |-- Attrib.thms); val varss = - OuterParse.and_list' - (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_source)))); + Parse.and_list' (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_source)))); in