changeset 48902 | 44a6967240b7 |
parent 48534 | 2307efbfc554 |
child 50486 | d5dc28fafd9d |
--- a/src/HOL/Tools/SMT/smt_solver.ML Thu Aug 23 12:55:23 2012 +0200 +++ b/src/HOL/Tools/SMT/smt_solver.ML Thu Aug 23 13:03:29 2012 +0200 @@ -96,7 +96,7 @@ SMT_Config.with_timeout ctxt (run ctxt name mk_cmd) input val _ = SMT_Config.trace_msg ctxt (pretty "Solver:") err - val ls = rev (snd (chop_while (equal "") (rev res))) + val ls = fst (take_suffix (equal "") res) val _ = SMT_Config.trace_msg ctxt (pretty "Result:") ls val _ = return_code <> 0 andalso