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