# 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]))