added function store_termination_rule to the signature, as it is used in Nominal2
--- 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,