src/HOL/Boogie/Tools/boogie_loader.ML
changeset 33497 39c9d0785911
parent 33465 8c489493e65e
child 33661 31a129cc0d10
     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)