--- a/src/HOL/SPARK/Tools/fdl_parser.ML Wed Mar 21 23:41:22 2012 +0100
+++ b/src/HOL/SPARK/Tools/fdl_parser.ML Thu Mar 22 10:10:02 2012 +0100
@@ -323,7 +323,7 @@
$$$ ":" -- identifier)) >> add_fun_decl) x;
fun declarations x =
- ($$$ "title" |-- subprogram_kind -- identifier --| $$$ ";" --
+ (the_identifier "title" |-- subprogram_kind -- identifier --| $$$ ";" --
(Scan.repeat ((type_decl || const_decl || var_decl || fun_decl) --|
!!! ($$$ ";")) >> (fn ds => fold I ds empty_decls)) --|
$$$ "end" --| $$$ ";") x;