src/HOL/Tools/Predicate_Compile/code_prolog.ML

     val renaming = fold mk_renaming vars []
   in ((rel, map (rename_vars_term renaming) args), rename_vars_prem renaming prem) end
   
 val rename_vars_program = map rename_vars_clause
 
+(* post processing of generated prolog program *)
+
+fun post_process ctxt options (p, constant_table) =
+  (p, constant_table)
+  |> (if #ensure_groundness options then
+        add_ground_predicates ctxt (#limited_types options)
+      else I)
+  |> add_limited_predicates (#limited_predicates options)
+  |> apfst (fold replace (#replacing options))
+  |> apfst (reorder_manually (#manual_reorder options))
+  |> apfst rename_vars_program
+
 (* code printer *)
 
 fun write_arith_op Plus = "+"
   | write_arith_op Minus = "-"
 

   
 (* calling external interpreter and getting results *)
 
 fun run (timeout, system) p (query_rel, args) vnames nsols =
   let
-    val p' = rename_vars_program p
-    val _ = tracing "Renaming variable names..."
     val renaming = fold mk_renaming (fold add_vars args vnames) [] 
     val vnames' = map (fn v => the (AList.lookup (op =) renaming v)) vnames
     val args' = map (rename_vars_term renaming) args
-    val prog = prelude system ^ query system nsols (query_rel, args') vnames' ^ write_program p'
+    val prog = prelude system ^ query system nsols (query_rel, args') vnames' ^ write_program p
     val _ = tracing ("Generated prolog program:\n" ^ prog)
     val solution = TimeLimit.timeLimit timeout (fn prog => Cache_IO.with_tmp_file "prolog_file" (fn prolog_file =>
       (File.write prolog_file prog; invoke system (Path.implode prolog_file)))) prog
     val _ = tracing ("Prolog returned solution(s):\n" ^ solution)
     val tss = parse_solutions solution

       Theory.copy (ProofContext.theory_of ctxt)
       |> Predicate_Compile.preprocess preprocess_options t
     val ctxt' = ProofContext.init_global thy'
     val _ = tracing "Generating prolog program..."
     val (p, constant_table) = generate (NONE, #ensure_groundness options) ctxt' name (* FIXME *)
-      |> (if #ensure_groundness options then
-          add_ground_predicates ctxt' (#limited_types options)
-        else I)
-      |> add_limited_predicates (#limited_predicates options)
-      |> apfst (fold replace (#replacing options))
-      |> apfst (reorder_manually (#manual_reorder options))
+      |> post_process ctxt' options
     val constant_table' = declare_consts (fold Term.add_const_names all_args []) constant_table
     val args' = map (translate_term ctxt constant_table') all_args
     val _ = tracing "Running prolog program..."
     val system_config = System_Config.get (Context.Proof ctxt)
     val tss = run (#timeout system_config, #prolog_system system_config)

     val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
     val thy3 = Predicate_Compile.preprocess preprocess_options (Const (full_constname, constT)) thy2
     val ctxt' = ProofContext.init_global thy3
     val _ = tracing "Generating prolog program..."
     val (p, constant_table) = generate (NONE, true) ctxt' full_constname
-      |> add_ground_predicates ctxt' (#limited_types options)
-      |> add_limited_predicates (#limited_predicates options)
-      |> apfst (fold replace (#replacing options))
-      |> apfst (reorder_manually (#manual_reorder options))
+      |> post_process ctxt' (set_ensure_groundness options)
     val _ = tracing "Running prolog program..."
     val system_config = System_Config.get (Context.Proof ctxt)
     val tss = run (#timeout system_config, #prolog_system system_config)
       p (translate_const constant_table full_constname, map (Var o fst) vs') (map fst vs') (SOME 1)
     val _ = tracing "Restoring terms..."