--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Jul 29 17:27:59 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Jul 29 18:16:35 2010 +0200
@@ -181,7 +181,8 @@
fun query_first rel vnames =
"eval :- once(" ^ rel ^ "(" ^ space_implode ", " vnames ^ ")),\n" ^
- "writef('" ^ implode (map (fn v => v ^ " = %w; ") vnames) ^"\\n', [" ^ space_implode ", " vnames ^ "]).\n"
+ "writef('" ^ space_implode ";" (map (fn v => v ^ " = %w") vnames) ^
+ "\\n', [" ^ space_implode ", " vnames ^ "]).\n"
fun query_firstn n rel vnames =
"eval :- findnsols(" ^ string_of_int n ^ ", (" ^ space_implode ", " vnames ^ "), " ^