src/HOL/Tools/inductive.ML
changeset 55111 5792f5106c40
parent 54883 dd04a8b654fc
child 55997 9dc5ce83202c
--- a/src/HOL/Tools/inductive.ML	Wed Jan 22 15:28:19 2014 +0100
+++ b/src/HOL/Tools/inductive.ML	Wed Jan 22 16:03:11 2014 +0100
@@ -591,7 +591,7 @@
 
 val ind_cases_setup =
   Method.setup @{binding ind_cases}
-    (Scan.lift (Scan.repeat1 Args.name_source --
+    (Scan.lift (Scan.repeat1 Args.name_inner_syntax --
       Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.binding) []) >>
       (fn (raw_props, fixes) => fn ctxt =>
         let