# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1351390959 0
# Node ID 4de92b4aa74a738ca89fad4f99894ce4390c31c2
# Parent  c163145dd40f7abc69834f2ce0d5e22b856716ba
added function store_termination_rule to the signature, as it is used in Nominal2

diff -r c163145dd40f -r 4de92b4aa74a src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Sat Oct 27 20:59:50 2012 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Sun Oct 28 02:22:39 2012 +0000
@@ -72,6 +72,7 @@
   structure Termination_Simps: NAMED_THMS
   val set_termination_prover : (Proof.context -> tactic) -> Context.generic -> Context.generic
   val get_termination_prover : Proof.context -> tactic
+  val store_termination_rule : thm -> Context.generic -> Context.generic
   datatype function_config = FunctionConfig of
    {sequential: bool,
     default: string option,