diff -r 077a2758ceb4 -r 59ef06cda7b9 src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Sun Sep 08 19:25:06 2013 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Sun Sep 08 22:32:47 2013 +0200
@@ -915,8 +915,9 @@
              (map (mk_domain_intro lthy globals R R_elim)) xclauses)
            else NONE
       in
-        FunctionResult {fs=[f], G=G, R=R, dom=dom, cases=complete_thm,
-          psimps=psimps, simple_pinducts=[simple_pinduct],
+        FunctionResult {fs=[f], G=G, R=R, dom=dom,
+          cases=[complete_thm], psimps=psimps, pelims=[],
+          simple_pinducts=[simple_pinduct],
           termination=total_intro, domintros=dom_intros}
       end
   in