diff -r 6cac9f48f96a -r f88eca2e9ebd src/HOL/SPARK/Tools/fdl_parser.ML
--- a/src/HOL/SPARK/Tools/fdl_parser.ML	Thu Jan 20 21:12:25 2011 +0100
+++ b/src/HOL/SPARK/Tools/fdl_parser.ML	Fri Jan 21 10:35:53 2011 +0100
@@ -302,7 +302,7 @@
    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 --| $$$ "]" --|
@@ -310,23 +310,23 @@
    || $$$ "record" |-- !!! (enum1 ";"
         (list1 identifier -- !!! ($$$ ":" |-- identifier)) --|
            $$$ "end") >> Record_Type
-   || $$$ "pending" >> K Pending_Type)) >> add_type_decl;
+   || $$$ "pending" >> K Pending_Type)) >> add_type_decl) x;
 
-val const_decl = $$$ "const" |-- !!! (identifier --| $$$ ":" -- identifier --|
-  $$$ "=" --| $$$ "pending") >> add_const_decl;
+fun const_decl x = ($$$ "const" |-- !!! (identifier --| $$$ ":" -- identifier --|
+  $$$ "=" --| $$$ "pending") >> add_const_decl) x;
 
-val var_decl = $$$ "var" |-- !!! (list1 identifier --| $$$ ":" -- identifier) >>
-  add_var_decl;
+fun var_decl x = ($$$ "var" |-- !!! (list1 identifier --| $$$ ":" -- identifier) >>
+  add_var_decl) x;
 
-val fun_decl = $$$ "function" |-- !!! (identifier --
+fun fun_decl x = ($$$ "function" |-- !!! (identifier --
   (Scan.optional ($$$ "(" |-- !!! (list1 identifier --| $$$ ")")) [] --|
-   $$$ ":" -- identifier)) >> add_fun_decl;
+   $$$ ":" -- identifier)) >> add_fun_decl) x;
 
-val declarations =
-  $$$ "title" |-- subprogram_kind -- identifier --| $$$ ";" --
+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 |>