--- a/src/Pure/Isar/isar_syn.ML Tue Sep 03 11:58:34 2013 +0200
+++ b/src/Pure/Isar/isar_syn.ML Tue Sep 03 13:09:15 2013 +0200
@@ -611,8 +611,9 @@
val _ =
Outer_Syntax.command @{command_spec "case"} "invoke local context"
((@{keyword "("} |--
- Parse.!!! (Parse.xname -- Scan.repeat (Parse.maybe Parse.binding) --| @{keyword ")"}) ||
- Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> (fn ((c, xs), atts) =>
+ Parse.!!! (Parse.position Parse.xname -- Scan.repeat (Parse.maybe Parse.binding)
+ --| @{keyword ")"}) ||
+ Parse.position Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> (fn ((c, xs), atts) =>
Toplevel.print o Toplevel.proof (Proof.invoke_case_cmd (c, xs, atts))));