# HG changeset patch
# User bulwahn
# Date 1283259726 -7200
# Node ID 8c2f5917164770784a0701caa066912f61290206
# Parent  363bfb2459179b624c029b5e6fc2944cc6e3fb2e
handling the quickcheck result no counterexample more correctly

diff -r 363bfb245917 -r 8c2f59171647 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Tue Aug 31 14:30:39 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Tue Aug 31 15:02:06 2010 +0200
@@ -621,8 +621,9 @@
         (l :: r :: []) => parse_term (unprefix " " r)
       | _ => raise Fail "unexpected equation in prolog output"
     fun parse_solution s = map dest_eq (space_explode ";" s)
+    val sols = case space_explode "\n" sol of [] => [] | s => fst (split_last s)  
   in
-    map parse_solution (fst (split_last (space_explode "\n" sol)))
+    map parse_solution sols
   end 
   
 (* calling external interpreter and getting results *)
@@ -816,10 +817,13 @@
       |> apfst (fold replace (#replacing options))
       |> apfst (reorder_manually (#manual_reorder options))
     val _ = tracing "Running prolog program..."
-    val [ts] = run (#prolog_system options)
+    val tss = run (#prolog_system options)
       p (translate_const constant_table full_constname) (map fst vs') (SOME 1)
     val _ = tracing "Restoring terms..."
-    val res = SOME (map (restore_term ctxt' constant_table) (ts ~~ Ts))
+    val res =
+      case tss of
+        [ts] => SOME (map (restore_term ctxt' constant_table) (ts ~~ Ts))
+      | _ => NONE
     val empty_report = ([], false)
   in
     (res, empty_report)