Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/SMT/smt_solver.ML
changeset 39811 0659e84bdc5f
parent 39809 dac3c3106746
child 40161 539d07b00e5f 
--- a/src/HOL/Tools/SMT/smt_solver.ML	Fri Oct 01 08:25:23 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Fri Oct 01 10:25:36 2010 +0200
@@ -160,7 +160,7 @@
     val (res, err) = with_timeout ctxt (run ctxt cmd args) input
     val _ = trace_msg ctxt (pretty "SMT solver:") err
 
-    val ls = rev (drop_while (equal "") (rev res))
+    val ls = rev (snd (chop_while (equal "") (rev res)))
     val _ = trace_msg ctxt (pretty "SMT result:") ls
   in ls end
isabelle