# HG changeset patch
# User boehmes
# Date 1257253658 -3600
# Node ID ab2f6574a2a6cfb01f90f1bf64a338d44b0f76c9
# Parent  5c1928d5db38c309b03aef388f2a0e07b740691e
ignore parsing errors, return empty assignment instead

diff -r 5c1928d5db38 -r ab2f6574a2a6 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 *)