diff -r 4d84fe96d5cb -r ee25a04fa06a src/HOL/Tools/Function/fun.ML
--- a/src/HOL/Tools/Function/fun.ML	Sun Oct 21 22:11:38 2012 +0200
+++ b/src/HOL/Tools/Function/fun.ML	Sun Oct 21 22:12:22 2012 +0200
@@ -157,7 +157,7 @@
       THEN auto_tac ctxt
     fun prove_termination lthy =
       Function.prove_termination NONE
-        (Function_Common.get_termination_prover lthy lthy) lthy
+        (Function_Common.get_termination_prover lthy) lthy
   in
     lthy
     |> add pat_completeness_auto |> snd