--- a/src/HOL/Tools/inductive.ML Wed Apr 27 19:55:42 2011 +0200
+++ b/src/HOL/Tools/inductive.ML Wed Apr 27 20:19:05 2011 +0200
@@ -552,10 +552,10 @@
val ind_cases_setup =
Method.setup @{binding ind_cases}
(Scan.lift (Scan.repeat1 Args.name_source --
- Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.name) []) >>
+ Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.binding) []) >>
(fn (raw_props, fixes) => fn ctxt =>
let
- val (_, ctxt') = Variable.add_fixes fixes ctxt;
+ val (_, ctxt') = Variable.add_fixes_binding fixes ctxt;
val props = Syntax.read_props ctxt' raw_props;
val ctxt'' = fold Variable.declare_term props ctxt';
val rules = Proof_Context.export ctxt'' ctxt (map (mk_cases ctxt'') props)