--- a/src/HOL/Fun_Def.thy Tue Jul 07 18:01:30 2015 +0200
+++ b/src/HOL/Fun_Def.thy Tue Jul 07 18:37:24 2015 +0200
@@ -304,7 +304,7 @@
ML_val -- "setup inactive"
{*
Context.theory_map (Function_Common.set_termination_prover
- (ScnpReconstruct.decomp_scnp_tac [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS]))
+ (K (ScnpReconstruct.decomp_scnp_tac [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS])))
*}
end
--- a/src/HOL/Tools/Function/fun.ML Tue Jul 07 18:01:30 2015 +0200
+++ b/src/HOL/Tools/Function/fun.ML Tue Jul 07 18:37:24 2015 +0200
@@ -158,8 +158,7 @@
Pat_Completeness.pat_completeness_tac ctxt 1
THEN auto_tac ctxt
fun prove_termination lthy =
- Function.prove_termination NONE
- (Function_Common.termination_prover_tac lthy) lthy
+ Function.prove_termination NONE (Function_Common.termination_prover_tac false lthy) lthy
in
lthy
|> add pat_completeness_auto |> snd
--- a/src/HOL/Tools/Function/function_common.ML Tue Jul 07 18:01:30 2015 +0200
+++ b/src/HOL/Tools/Function/function_common.ML Tue Jul 07 18:37:24 2015 +0200
@@ -82,8 +82,9 @@
val store_termination_rule : thm -> Context.generic -> Context.generic
val get_functions : Proof.context -> (term * info) Item_Net.T
val add_function_data : info -> Context.generic -> Context.generic
- val termination_prover_tac : Proof.context -> tactic
- val set_termination_prover : (Proof.context -> tactic) -> Context.generic -> Context.generic
+ val termination_prover_tac : bool -> Proof.context -> tactic
+ val set_termination_prover : (bool -> Proof.context -> tactic) -> Context.generic ->
+ Context.generic
val get_preproc: Proof.context -> preproc
val set_preproc: preproc -> Context.generic -> Context.generic
datatype function_result = FunctionResult of
@@ -262,7 +263,7 @@
type T =
thm list *
(term * info) Item_Net.T *
- (Proof.context -> tactic) *
+ (bool -> Proof.context -> tactic) *
preproc
val empty: T =
([],
@@ -288,7 +289,7 @@
(Data.map o @{apply 4(2)}) (fold (fn f => Item_Net.update (f, info)) fs)
#> store_termination_rule termination
-fun termination_prover_tac ctxt = #3 (Data.get (Context.Proof ctxt)) ctxt
+fun termination_prover_tac quiet ctxt = #3 (Data.get (Context.Proof ctxt)) quiet ctxt
val set_termination_prover = Data.map o @{apply 4(3)} o K
val get_preproc = #4 o Data.get o Context.Proof
--- a/src/HOL/Tools/Function/lexicographic_order.ML Tue Jul 07 18:01:30 2015 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Tue Jul 07 18:37:24 2015 +0200
@@ -216,6 +216,6 @@
val _ =
Theory.setup
(Context.theory_map
- (Function_Common.set_termination_prover (lexicographic_order_tac false)))
+ (Function_Common.set_termination_prover lexicographic_order_tac))
end;