src/HOL/Tools/Predicate_Compile/code_prolog.ML
changeset 73277 0110e2e2964c
parent 73235 4e631963fe24
child 73285 0e7a3c055f39
--- 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 *)