# HG changeset patch
# User wenzelm
# Date 1392645549 -3600
# Node ID 6ec3c2c38650f888a42e24f2d93eeb799f6c08cf
# Parent  56ebc4d4d0089ab6a9fede8f3d454e1339af5b21
made SML/NJ happy;

diff -r 56ebc4d4d008 -r 6ec3c2c38650 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Feb 17 14:07:26 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Feb 17 14:59:09 2014 +0100
@@ -684,8 +684,6 @@
     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
-
 
 (* limit computation globally by some threshold *)
 
@@ -706,7 +704,7 @@
 
 (* post processing of generated prolog program *)
 
-fun post_process ctxt options const_name (p, constant_table) =
+fun post_process ctxt (options: code_options) const_name (p, constant_table) =
   (p, constant_table)
   |> (case #limit_globally options of
         SOME limit => limit_globally limit const_name
@@ -719,7 +717,7 @@
   |> tap (fn _ => tracing "Replacing predicates...")
   |> apfst (fold replace (#replacing options))
   |> apfst (reorder_manually (#manual_reorder options))
-  |> apfst rename_vars_program
+  |> apfst (map rename_vars_clause)
 
 
 (* code printer *)