# HG changeset patch
# User blanchet
# Date 1436287044 -7200
# Node ID 5a6cd25605495442843d6bbf1bbccc405b218bd8
# Parent  9ce7463350a90adf515a369aa86234f646800889
have the installed termination prover take a 'quiet' flag

diff -r 9ce7463350a9 -r 5a6cd2560549 src/HOL/Fun_Def.thy
--- 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
diff -r 9ce7463350a9 -r 5a6cd2560549 src/HOL/Tools/Function/fun.ML
--- 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
diff -r 9ce7463350a9 -r 5a6cd2560549 src/HOL/Tools/Function/function_common.ML
--- 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
diff -r 9ce7463350a9 -r 5a6cd2560549 src/HOL/Tools/Function/lexicographic_order.ML
--- 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;