# HG changeset patch
# User wenzelm
# Date 1330809472 -3600
# Node ID 7cc567fd2789c0d5ffce678d52576704efe194e6
# Parent  1ce61ee1571a689794ffb58ec3811c35103e9a69
tuned;

diff -r 1ce61ee1571a -r 7cc567fd2789 src/HOL/SPARK/Tools/fdl_parser.ML
--- 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 |>