# HG changeset patch
# User bulwahn
# Date 1256396142 -7200
# Node ID cef39362ce56f052220e5d677671fc3b8106a337
# Parent  7eac458c2b22b7c416102b5f18d05095b85fe705
removed unnecessary argument rpred in code_pred function

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
diff -r 7eac458c2b22 -r cef39362ce56 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -7,8 +7,8 @@
 signature PREDICATE_COMPILE_CORE =
 sig
   val setup: theory -> theory
-  val code_pred: Predicate_Compile_Aux.options -> int list list option -> bool -> string -> Proof.context -> Proof.state
-  val code_pred_cmd: Predicate_Compile_Aux.options -> int list list option -> bool -> string -> Proof.context -> Proof.state
+  val code_pred: Predicate_Compile_Aux.options -> int list list option -> string -> Proof.context -> Proof.state
+  val code_pred_cmd: Predicate_Compile_Aux.options -> int list list option -> string -> Proof.context -> Proof.state
   type smode = (int * int list option) list
   type mode = smode option list * smode
   datatype tmode = Mode of mode * smode * tmode option list;
@@ -2308,7 +2308,7 @@
 fun add_equations_of steps options expected_modes prednames thy =
   let
     val _ = print_step options ("Starting predicate compiler for predicates " ^ commas prednames ^ "...")
-    val _ = tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames)))
+    val _ = Output.tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames)))
       (*val _ = check_intros_elim_match thy prednames*)
       (*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*)
     val (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) =
@@ -2425,7 +2425,7 @@
   (*FIXME why distinguished attribute for cases?*)
 
 (* TODO: make TheoryDataFun to GenericDataFun & remove duplication of local theory and theory *)
-fun generic_code_pred prep_const options modes rpred raw_const lthy =
+fun generic_code_pred prep_const options modes raw_const lthy =
   let
     val thy = ProofContext.theory_of lthy
     val const = prep_const thy raw_const
@@ -2454,7 +2454,7 @@
           (ProofContext.init (ProofContext.theory_of goal_ctxt)) (map the_single thms)
       in
         goal_ctxt |> LocalTheory.theory (fold set_elim global_thms #>
-          (if rpred then
+          (if is_rpred options then
             (add_equations options NONE [const] #>
              add_sizelim_equations options NONE [const] #> add_quickcheck_equations options NONE [const])
            else add_equations options modes [const]))