| changeset 27809 | a1e409db516b |
| parent 27328 | 1f0ac20db386 |
| child 27882 | eaa9fef9f4c1 |
--- a/src/Tools/induct_tacs.ML Sat Aug 09 12:28:13 2008 +0200 +++ b/src/Tools/induct_tacs.ML Sat Aug 09 22:43:46 2008 +0200 @@ -117,7 +117,7 @@ val opt_rules = Scan.option (rule_spec |-- Attrib.thms); val varss = - Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name)))); + OuterParse.and_list' (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name)))); in