src/HOL/SPARK/Tools/fdl_parser.ML

 fun add_fun_decl decl {types, vars, consts, funs} =
   {types = types, vars = vars, consts = consts,
    funs = update decl funs}
   handle Symtab.DUP s => error ("Duplicate function " ^ s);
 
-val type_decl = $$$ "type" |-- !!! (identifier --| $$$ "=" --
+fun type_decl x = ($$$ "type" |-- !!! (identifier --| $$$ "=" --
   (   identifier >> Basic_Type
    || $$$ "(" |-- !!! (list1 identifier --| $$$ ")") >> Enum_Type
    || $$$ "array" |-- !!! ($$$ "[" |-- list1 identifier --| $$$ "]" --|
         $$$ "of" -- identifier) >> Array_Type
    || $$$ "record" |-- !!! (enum1 ";"
         (list1 identifier -- !!! ($$$ ":" |-- identifier)) --|
            $$$ "end") >> Record_Type
-   || $$$ "pending" >> K Pending_Type)) >> add_type_decl;
-
-val const_decl = $$$ "const" |-- !!! (identifier --| $$$ ":" -- identifier --|
-  $$$ "=" --| $$$ "pending") >> add_const_decl;
-
-val var_decl = $$$ "var" |-- !!! (list1 identifier --| $$$ ":" -- identifier) >>
-  add_var_decl;
-
-val fun_decl = $$$ "function" |-- !!! (identifier --
+   || $$$ "pending" >> K Pending_Type)) >> add_type_decl) x;
+
+fun const_decl x = ($$$ "const" |-- !!! (identifier --| $$$ ":" -- identifier --|
+  $$$ "=" --| $$$ "pending") >> add_const_decl) x;
+
+fun var_decl x = ($$$ "var" |-- !!! (list1 identifier --| $$$ ":" -- identifier) >>
+  add_var_decl) x;
+
+fun fun_decl x = ($$$ "function" |-- !!! (identifier --
   (Scan.optional ($$$ "(" |-- !!! (list1 identifier --| $$$ ")")) [] --|
-   $$$ ":" -- identifier)) >> add_fun_decl;
-
-val declarations =
-  $$$ "title" |-- subprogram_kind -- identifier --| $$$ ";" --
+   $$$ ":" -- identifier)) >> add_fun_decl) x;
+
+fun declarations x =
+ ($$$ "title" |-- subprogram_kind -- identifier --| $$$ ";" --
   (Scan.repeat ((type_decl || const_decl || var_decl || fun_decl) --|
      !!! ($$$ ";")) >> (fn ds => apply ds empty_decls)) --|
-  $$$ "end" --| $$$ ";"
+  $$$ "end" --| $$$ ";") x;
 
 fun parse_declarations pos s =
   s |>
   Fdl_Lexer.tokenize (Scan.succeed ()) Fdl_Lexer.curly_comment pos |>
   snd |> filter Fdl_Lexer.is_proper |>