# HG changeset patch
# User boehmes
# Date 1257540800 -3600
# Node ID 39c9d0785911b81235c9ff53f2ca5b158431db5f
# Parent  5212eccda1cb856f0e0686807706ae9fa3764309
made SML/NJ happy

diff -r 5212eccda1cb -r 39c9d0785911 src/HOL/Boogie/Tools/boogie_loader.ML
--- a/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Nov 06 21:20:37 2009 +0100
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Nov 06 21:53:20 2009 +0100
@@ -293,8 +293,8 @@
 fun read_int' s = (case read_int (explode s) of (i, []) => SOME i | _ => NONE)
 
 fun $$$ s = Scan.one (fn (_, Token s') => s = s' | _ => false)
-val str = Scan.some (fn (_, Token s) => SOME s | _ => NONE)
-val num = Scan.some (fn (_, Token s) => read_int' s | _ => NONE)
+fun str st = Scan.some (fn (_, Token s) => SOME s | _ => NONE) st
+fun num st = Scan.some (fn (_, Token s) => read_int' s | _ => NONE) st
 
 fun scan_line key scan =
   $$$ key |-- scan --| Scan.one (fn (_, Newline) => true | _ => false)
diff -r 5212eccda1cb -r 39c9d0785911 src/HOL/SMT/Tools/z3_model.ML
--- a/src/HOL/SMT/Tools/z3_model.ML	Fri Nov 06 21:20:37 2009 +0100
+++ b/src/HOL/SMT/Tools/z3_model.ML	Fri Nov 06 21:53:20 2009 +0100
@@ -55,7 +55,8 @@
 val value = mapping |-- expr
 
 val args_case = Scan.repeat expr -- value
-val else_case = space -- Scan.this_string "else" |-- value >> pair []
+val else_case = space -- Scan.this_string "else" |-- value >>
+  pair ([] : expr list)
 
 val func =
   let fun cases st = (else_case >> single || args_case ::: cases) st