diff -r 71df93ff010d -r 80c00a851de5 src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Sun Jun 16 01:39:00 2013 +0200
+++ b/src/HOL/Tools/Function/mutual.ML	Sun Jun 16 22:56:44 2013 +0200
@@ -252,7 +252,7 @@
   let
     val result = inner_cont proof
     val FunctionResult {G, R, cases, psimps, simple_pinducts=[simple_pinduct],
-      termination, domintros, ...} = result
+      termination, domintros, dom, ...} = result
 
     val (all_f_defs, fs) =
       map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} =>
@@ -272,7 +272,7 @@
     val mtermination = full_simplify rew_simpset termination
     val mdomintros = Option.map (map (full_simplify rew_simpset)) domintros
   in
-    FunctionResult { fs=fs, G=G, R=R,
+    FunctionResult { fs=fs, G=G, R=R, dom=dom,
       psimps=mpsimps, simple_pinducts=minducts,
       cases=cases, termination=mtermination,
       domintros=mdomintros}