src/HOL/Tools/Function/function.ML

     val ((goal_state, cont), lthy') =
       Function_Mutual.prepare_function_mutual config defname fixes eqs lthy
 
     fun afterqed [[proof]] lthy =
       let
-        val FunctionResult {fs, R, psimps, simple_pinducts,
+        val FunctionResult {fs, R, dom, psimps, simple_pinducts,
           termination, domintros, cases, ...} =
           cont (Thm.close_derivation proof)
 
         val fnames = map (fst o fst) fixes
         fun qualify n = Binding.name n

           ||> (case domintros of NONE => I | SOME thms => 
                    Local_Theory.note ((qualify "domintros", []), thms) #> snd)
 
         val info = { add_simps=addsmps, case_names=cnames, psimps=psimps',
           pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
-          fs=fs, R=R, defname=defname, is_partial=true, cases=cases'}
+          fs=fs, R=R, dom=dom, defname=defname, is_partial=true, cases=cases'}
 
         val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes)
       in
         (info,
          lthy |> Local_Theory.declaration {syntax = false, pervasive = false}

           (case import_last_function lthy of
             SOME info => info
           | NONE => error "Not a function"))
 
     val { termination, fs, R, add_simps, case_names, psimps,
-      pinducts, defname, cases, ...} = info
+      pinducts, defname, cases, dom, ...} = info
     val domT = domain_type (fastype_of R)
     val goal = HOLogic.mk_Trueprop (HOLogic.mk_all ("x", domT, mk_acc domT R $ Free ("x", domT)))
     fun afterqed [[totality]] lthy =
       let
         val totality = Thm.close_derivation totality

            ((qualify "induct",
              [Attrib.internal (K (Rule_Cases.case_names case_names))]),
             tinduct)
         |-> (fn (simps, (_, inducts)) => fn lthy =>
           let val info' = { is_partial=false, defname=defname, add_simps=add_simps,
-            case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts,
+            case_names=case_names, fs=fs, R=R, dom=dom, psimps=psimps, pinducts=pinducts,
             simps=SOME simps, inducts=SOME inducts, termination=termination, cases=cases }
           in
             (info',
              lthy 
              |> Local_Theory.declaration {syntax = false, pervasive = false}