# HG changeset patch
# User wenzelm
# Date 1295602553 -3600
# Node ID f88eca2e9ebdaf1d20cef5660256e5858dd94d1e
# Parent  6cac9f48f96a0ddb923678616f4224db2b0b283a
made SML/NJ happy;

diff -r 6cac9f48f96a -r f88eca2e9ebd src/HOL/Boogie/Tools/boogie_vcs.ML
--- a/src/HOL/Boogie/Tools/boogie_vcs.ML	Thu Jan 20 21:12:25 2011 +0100
+++ b/src/HOL/Boogie/Tools/boogie_vcs.ML	Fri Jan 21 10:35:53 2011 +0100
@@ -276,9 +276,9 @@
 structure VCs_Data = Theory_Data
 (
   type T = vcs_data
-  val empty = make_vcs_data (NONE, K I, [])
+  val empty : T = make_vcs_data (NONE, K I, [])
   val extend = I
-  fun merge ({vcs=vcs1, filters=fs1, ...}, {vcs=vcs2, filters=fs2, ...}) =
+  fun merge ({vcs=vcs1, filters=fs1, ...} : T, {vcs=vcs2, filters=fs2, ...} : T) =
     (case (vcs1, vcs2) of
       (NONE, NONE) =>
         make_vcs_data (NONE, K I, Ord_List.merge serial_ord (fs1, fs2))
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 |>