ignore parsing errors, return empty assignment instead
authorboehmes
Tue, 03 Nov 2009 14:07:38 +0100
changeset 33417 ab2f6574a2a6
parent 33405 5c1928d5db38
child 33418 1312e8337ce5
ignore parsing errors, return empty assignment instead
src/HOL/SMT/Tools/z3_model.ML
--- a/src/HOL/SMT/Tools/z3_model.ML	Tue Nov 03 10:36:20 2009 +0100
+++ b/src/HOL/SMT/Tools/z3_model.ML	Tue Nov 03 14:07:38 2009 +0100
@@ -66,8 +66,8 @@
 
 fun read_cex ls =
   explode (cat_lines ls)
-  |> Scan.catch (Scan.finite Symbol.stopper (Scan.error cex))
-  |> fst
+  |> try (fst o Scan.finite Symbol.stopper cex)
+  |> the_default []
 
 
 (* translation into terms *)