--- a/src/HOL/SPARK/Tools/fdl_parser.ML Sat Mar 03 22:11:51 2012 +0100
+++ b/src/HOL/SPARK/Tools/fdl_parser.ML Sat Mar 03 22:17:52 2012 +0100
@@ -325,7 +325,7 @@
fun declarations x =
($$$ "title" |-- subprogram_kind -- identifier --| $$$ ";" --
(Scan.repeat ((type_decl || const_decl || var_decl || fun_decl) --|
- !!! ($$$ ";")) >> (fn ds => apply ds empty_decls)) --|
+ !!! ($$$ ";")) >> (fn ds => fold I ds empty_decls)) --|
$$$ "end" --| $$$ ";") x;
fun parse_declarations pos s =
@@ -371,7 +371,7 @@
val rules =
parse_all (rule >> (apfst o cons) || rule_family >> (apsnd o cons)) >>
- (fn rls => apply (rev rls) ([], []));
+ (fn rls => fold_rev I rls ([], []));
fun parse_rules pos s =
s |>