src/Tools/induct_tacs.ML
changeset 27882 eaa9fef9f4c1
parent 27809 a1e409db516b
child 28308 d4396a28fb29
--- a/src/Tools/induct_tacs.ML	Thu Aug 14 21:06:07 2008 +0200
+++ b/src/Tools/induct_tacs.ML	Fri Aug 15 15:50:44 2008 +0200
@@ -117,13 +117,14 @@
 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))));
+  OuterParse.and_list'
+    (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name_source))));
 
 in
 
 val setup =
   Method.add_methods
-   [("case_tac", Method.goal_args_ctxt' (Scan.lift Args.name -- opt_rule) gen_case_tac,
+   [("case_tac", Method.goal_args_ctxt' (Scan.lift Args.name_source -- opt_rule) gen_case_tac,
       "unstructured case analysis on types"),
     ("induct_tac", Method.goal_args_ctxt' (varss -- opt_rules) gen_induct_tac,
       "unstructured induction on types")];