src/HOL/Tools/SMT/cvc3_solver.ML
changeset 39809 dac3c3106746
parent 36899 bcd6fce5bf06
child 39811 0659e84bdc5f
--- a/src/HOL/Tools/SMT/cvc3_solver.ML	Thu Sep 30 09:45:18 2010 +0200
+++ b/src/HOL/Tools/SMT/cvc3_solver.ML	Thu Sep 30 18:37:29 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 (dropwhile empty_line output)
+    val (l, _) = split_first (drop_while empty_line output)
   in
     if is_unsat l then @{cprop False}
     else if is_sat l then raise_cex true