# HG changeset patch
# User wenzelm
# Date 1612732779 -3600
# Node ID 4e631963fe2420f3708313db0c2fa3a262da0d2e
# Parent  da0ee7fbc06826a3af9dde61ae6d0afec3de4296
more complete solutions (amending 4d36070bdbf4);

diff -r da0ee7fbc068 -r 4e631963fe24 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sun Feb 07 21:27:48 2021 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sun Feb 07 22:19:39 2021 +0100
@@ -865,10 +865,7 @@
         (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 Library.trim_split_lines sol of [] => [] | s => fst (split_last s))
-  in
-    map parse_solution sols
-  end
+  in map parse_solution (Library.trim_split_lines sol) end
 
 
 (* calling external interpreter and getting results *)