--- a/src/HOL/Tools/Function/function_common.ML Fri Aug 27 10:57:32 2010 +0200
+++ b/src/HOL/Tools/Function/function_common.ML Fri Aug 27 12:57:55 2010 +0200
@@ -164,7 +164,7 @@
structure Termination_Simps = Named_Thms
(
val name = "termination_simp"
- val description = "Simplification rule for termination proofs"
+ val description = "simplification rules for termination proofs"
)
@@ -175,7 +175,7 @@
type T = Proof.context -> tactic
val empty = (fn _ => error "Termination prover not configured")
val extend = I
- fun merge (a, b) = b (* FIXME ? *)
+ fun merge (a, _) = a
)
val set_termination_prover = TerminationProver.put