diff -r 54065cbf7134 -r 0110e2e2964c src/HOL/Tools/Predicate_Compile/code_prolog.ML --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Feb 22 15:20:45 2021 +0100 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Mon Feb 22 15:24:04 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) - in map parse_solution (Library.trim_split_lines sol) end + in map parse_solution (split_lines sol) end (* calling external interpreter and getting results *)