# HG changeset patch
# User berghofe
# Date 1332407402 -3600
# Node ID d04b38d4035b305a978809b4ded55765175a177d
# Parent  3031603233e3eedbf8a2796b1237c6467bb0652e
No longer treat "title" as FDL keyword

diff -r 3031603233e3 -r d04b38d4035b src/HOL/SPARK/Tools/fdl_lexer.ML
--- a/src/HOL/SPARK/Tools/fdl_lexer.ML	Wed Mar 21 23:41:22 2012 +0100
+++ b/src/HOL/SPARK/Tools/fdl_lexer.ML	Thu Mar 22 10:10:02 2012 +0100
@@ -96,7 +96,6 @@
 
 val lexicon = Scan.make_lexicon (map raw_explode
   ["rule_family",
-   "title",
    "For",
    ":",
    "[",
diff -r 3031603233e3 -r d04b38d4035b src/HOL/SPARK/Tools/fdl_parser.ML
--- 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;