diff -r 05cb83f083b9 -r 9312710451f5 src/HOL/Tools/Function/fun.ML
--- a/src/HOL/Tools/Function/fun.ML	Fri Dec 19 22:53:43 2014 +0100
+++ b/src/HOL/Tools/Function/fun.ML	Fri Dec 19 23:01:46 2014 +0100
@@ -160,7 +160,7 @@
       THEN auto_tac ctxt
     fun prove_termination lthy =
       Function.prove_termination NONE
-        (Function_Common.get_termination_prover lthy) lthy
+        (Function_Common.termination_prover_tac lthy) lthy
   in
     lthy
     |> add pat_completeness_auto |> snd