diff -r 030b930d1ac8 -r 4d36070bdbf4 src/HOL/Tools/Predicate_Compile/code_prolog.ML --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sun Feb 07 20:44:44 2021 +0100 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Sun Feb 07 21:25:21 2021 +0100 @@ -865,7 +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 space_explode "\n" sol of [] => [] | s => fst (split_last s)) + val sols = (case Library.trim_split_lines sol of [] => [] | s => fst (split_last s)) in map parse_solution sols end