# 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)