diff -r 772ed73e1d61 -r 73ed9f18fdd3 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Wed Apr 28 10:31:15 2010 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Wed Apr 28 11:52:04 2010 +0200
@@ -172,7 +172,7 @@
 
 structure TerminationProver = Generic_Data
 (
-  type T = Proof.context -> Proof.method
+  type T = Proof.context -> tactic
   val empty = (fn _ => error "Termination prover not configured")
   val extend = I
   fun merge (a, b) = b  (* FIXME ? *)