made SML/NJ happy
authorboehmes
Fri Nov 06 21:53:20 2009 +0100 (2009-11-06)
changeset 3349739c9d0785911
parent 33496 5212eccda1cb
child 33501 31872dd275c8
made SML/NJ happy
src/HOL/Boogie/Tools/boogie_loader.ML
src/HOL/SMT/Tools/z3_model.ML
     1.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Nov 06 21:20:37 2009 +0100
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Nov 06 21:53:20 2009 +0100
     1.3 @@ -293,8 +293,8 @@
     1.4  fun read_int' s = (case read_int (explode s) of (i, []) => SOME i | _ => NONE)
     1.5  
     1.6  fun $$$ s = Scan.one (fn (_, Token s') => s = s' | _ => false)
     1.7 -val str = Scan.some (fn (_, Token s) => SOME s | _ => NONE)
     1.8 -val num = Scan.some (fn (_, Token s) => read_int' s | _ => NONE)
     1.9 +fun str st = Scan.some (fn (_, Token s) => SOME s | _ => NONE) st
    1.10 +fun num st = Scan.some (fn (_, Token s) => read_int' s | _ => NONE) st
    1.11  
    1.12  fun scan_line key scan =
    1.13    $$$ key |-- scan --| Scan.one (fn (_, Newline) => true | _ => false)
     2.1 --- a/src/HOL/SMT/Tools/z3_model.ML	Fri Nov 06 21:20:37 2009 +0100
     2.2 +++ b/src/HOL/SMT/Tools/z3_model.ML	Fri Nov 06 21:53:20 2009 +0100
     2.3 @@ -55,7 +55,8 @@
     2.4  val value = mapping |-- expr
     2.5  
     2.6  val args_case = Scan.repeat expr -- value
     2.7 -val else_case = space -- Scan.this_string "else" |-- value >> pair []
     2.8 +val else_case = space -- Scan.this_string "else" |-- value >>
     2.9 +  pair ([] : expr list)
    2.10  
    2.11  val func =
    2.12    let fun cases st = (else_case >> single || args_case ::: cases) st