# HG changeset patch
# User blanchet
# Date 1273933254 -7200
# Node ID b4417ddad979a5dca2976b4b12d471ea7a4cb9d0
# Parent  dbd39471211c048143e2a2fe66ffe18476d578d7
make SML/NJ happy

diff -r dbd39471211c -r b4417ddad979 src/HOL/Tools/SMT/smt_solver.ML
--- 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)
diff -r dbd39471211c -r b4417ddad979 src/HOL/Tools/SMT/z3_proof_parser.ML
--- 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