diff -r 7eac458c2b22 -r cef39362ce56 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -131,10 +131,10 @@
           | NONE => const
         val _ = print_step options "Starting Predicate Compile Core..."
       in
-        Predicate_Compile_Core.code_pred options modes (is_rpred options) const lthy'
+        Predicate_Compile_Core.code_pred options modes const lthy'
       end
     else
-      Predicate_Compile_Core.code_pred_cmd options modes (is_rpred options) raw_const lthy
+      Predicate_Compile_Core.code_pred_cmd options modes raw_const lthy
   end
 
 val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup