src/HOL/Tools/Predicate_Compile/code_prolog.ML
changeset 73277 0110e2e2964c
parent 73235 4e631963fe24
child 73285 0e7a3c055f39
equal deleted inserted replaced
73276:54065cbf7134 73277:0110e2e2964c
   863     fun dest_eq s =
   863     fun dest_eq s =
   864       (case space_explode "=" s of
   864       (case space_explode "=" s of
   865         (l :: r :: []) => parse_term (unprefix " " r)
   865         (l :: r :: []) => parse_term (unprefix " " r)
   866       | _ => raise Fail "unexpected equation in prolog output")
   866       | _ => raise Fail "unexpected equation in prolog output")
   867     fun parse_solution s = map dest_eq (space_explode ";" s)
   867     fun parse_solution s = map dest_eq (space_explode ";" s)
   868   in map parse_solution (Library.trim_split_lines sol) end
   868   in map parse_solution (split_lines sol) end
   869 
   869 
   870 
   870 
   871 (* calling external interpreter and getting results *)
   871 (* calling external interpreter and getting results *)
   872 
   872 
   873 fun run ctxt p (query_rel, args) vnames nsols =
   873 fun run ctxt p (query_rel, args) vnames nsols =