# HG changeset patch
# User wenzelm
# Date 1612729521 -3600
# Node ID 4d36070bdbf49e6ebf8500e2a9abd19d93d252d7
# Parent  030b930d1ac83e7d45cf3917849222c64d47dfd5
more robust: accommodate output lines produced by Scala "bash_process";

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