diff -r 8da6846b87d9 -r 2a9d0ec8c10d src/HOL/Tools/Function/fun.ML
--- a/src/HOL/Tools/Function/fun.ML	Thu Apr 29 23:55:43 2010 +0200
+++ b/src/HOL/Tools/Function/fun.ML	Fri Apr 30 13:47:39 2010 +0200
@@ -151,7 +151,7 @@
     lthy
     |> add fixes statements config pat_completeness_auto |> snd
     |> Local_Theory.restore
-    |> prove_termination
+    |> prove_termination |> snd
   end
 
 val add_fun = gen_add_fun Function.add_function