diff -r 5c9fe600525e -r 0659e84bdc5f src/HOL/Tools/SMT/yices_solver.ML
--- a/src/HOL/Tools/SMT/yices_solver.ML	Fri Oct 01 08:25:23 2010 +0200
+++ b/src/HOL/Tools/SMT/yices_solver.ML	Fri Oct 01 10:25:36 2010 +0200
@@ -23,7 +23,7 @@
   let
     val empty_line = (fn "" => true | _ => false)
     val split_first = (fn [] => ("", []) | l :: ls => (l, ls))
-    val (l, _) = split_first (drop_while empty_line output)
+    val (l, _) = split_first (snd (chop_while empty_line output))
   in
     if String.isPrefix "unsat" l then @{cprop False}
     else if String.isPrefix "sat" l then raise_cex true