src/HOL/Tools/Predicate_Compile/code_prolog.ML

     "writelist([(" ^ space_implode ", " vnames ^ ")|SolutionTail]) :- " ^
     "writef('" ^ space_implode ";" (map (fn v => v ^ " = %w") vnames) ^
     "\\n', [" ^ space_implode ", " vnames ^ "]), writelist(SolutionTail).\n"
   
 val swi_prolog_prelude =
-  "#!/usr/bin/swipl -q -t main -f\n\n" ^  (* FIXME hardwired executable!? *)
   ":- use_module(library('dialect/ciao/aggregates')).\n" ^
   ":- style_check(-singleton).\n" ^
   ":- style_check(-discontiguous).\n" ^
   ":- style_check(-atom).\n\n" ^
   "main :- catch(eval, E, (print_message(error, E), fail)), halt.\n" ^

   "eval :- once(" ^ rel ^ "(" ^ space_implode ", " (map write_term args) ^ ")),\n" ^
   "format('" ^ space_implode ";" (map (fn v => v ^ " = ~w") vnames) ^
   "\\n', [" ^ space_implode ", " vnames ^ "]).\n"
 
 val yap_prelude =
-  "#!/usr/bin/yap -L\n\n" ^
   ":- initialization(eval).\n"
 
 (* system-dependent query, prelude and invocation *)
 
 fun query system nsols = 

 
 fun invoke system file =
   let
     val (env_var, cmd) =
       (case system of
-        SWI_PROLOG => ("ISABELLE_SWIPL", "\"$ISABELLE_SWIPL\" -f ")
+        SWI_PROLOG => ("ISABELLE_SWIPL", "\"$ISABELLE_SWIPL\" -q -t main -f ")
       | YAP => ("ISABELLE_YAP", "\"$ISABELLE_YAP\" -L "))
   in
     if getenv env_var = "" then
       (warning (env_var ^ " not set; could not execute code for " ^ string_of_system system); "")
     else