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