--- a/src/HOL/Tools/SMT/smt_solver.ML Sat May 15 13:31:25 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML Sat May 15 16:20:54 2010 +0200
@@ -166,7 +166,7 @@
end
-fun trace_recon_data ctxt {typs, terms, ...} =
+fun trace_recon_data ctxt ({typs, terms, ...} : SMT_Translate.recon) =
let
fun pretty_eq n p = Pretty.block [Pretty.str n, Pretty.str " = ", p]
fun pretty_typ (n, T) = pretty_eq n (Syntax.pretty_typ ctxt T)
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML Sat May 15 13:31:25 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML Sat May 15 16:20:54 2010 +0200
@@ -285,15 +285,15 @@
"4" => SOME 4 | "5" => SOME 5 | "6" => SOME 6 | "7" => SOME 7 |
"8" => SOME 8 | "9" => SOME 9 | _ => NONE)
-val digits = Scan.lift (Scan.many1 Symbol.is_ascii_digit) >> implode
-val nat_num = Scan.lift (Scan.repeat1 (Scan.some digit)) >> (fn ds =>
- fold (fn d => fn i => i * 10 + d) ds 0)
-val int_num = Scan.optional ($$ "-" >> K (fn i => ~i)) I :|--
- (fn sign => nat_num >> sign)
+fun digits st = (Scan.lift (Scan.many1 Symbol.is_ascii_digit) >> implode) st
+fun nat_num st = (Scan.lift (Scan.repeat1 (Scan.some digit)) >> (fn ds =>
+ fold (fn d => fn i => i * 10 + d) ds 0)) st
+fun int_num st = (Scan.optional ($$ "-" >> K (fn i => ~i)) I :|--
+ (fn sign => nat_num >> sign)) st
val is_char = Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf
member (op =) (explode "_+*-/%~=<>$&|?!.@^#")
-val name = Scan.lift (Scan.many1 is_char) >> implode
+fun name st = (Scan.lift (Scan.many1 is_char) >> implode) st
fun sym st =
(name -- Scan.optional (bra (seps_by ($$ ":") sym)) [] >> I.Sym) st