src/HOL/Tools/SMT/cvc3_solver.ML

--- a/src/HOL/Tools/SMT/cvc3_solver.ML	Fri Oct 01 08:25:23 2010 +0200
+++ b/src/HOL/Tools/SMT/cvc3_solver.ML	Fri Oct 01 10:25:36 2010 +0200
@@ -27,7 +27,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 is_unsat l then @{cprop False}
     else if is_sat l then raise_cex true