diff -r c421cfe2eada -r abe92b33ac9f src/HOL/Tools/Function/function_common.ML
--- 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