--- 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)
--- 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