src/HOL/Tools/Function/function.ML

           |> Binding.qualify true defname
         val conceal_partial = if partials then I else Binding.conceal
 
         val addsmps = add_simps fnames post sort_cont
 
-        val (((psimps', [pinducts']), (_, [termination'])), lthy) =
+        val ((((psimps', [pinducts']), [termination']), [cases']), lthy) =
           lthy
           |> addsmps (conceal_partial o Binding.qualify false "partial")
                "psimps" conceal_partial psimp_attribs psimps
           ||>> Local_Theory.notes [((conceal_partial (qualify "pinduct"), []),
                 simple_pinducts |> map (fn th => ([th],
                  [Attrib.internal (K (Rule_Cases.case_names cnames)),
                   Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th))),
                   Attrib.internal (K (Induct.induct_pred ""))])))]
-          ||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination])
-          ||> (snd o Local_Theory.note ((qualify "cases",
+          ||>> (apfst snd o Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination]))
+          ||>> (apfst snd o Local_Theory.note ((qualify "cases",
                  [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
           ||> (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 }
+          fs=fs, R=R, 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, ...} = info
+      pinducts, defname, cases, ...} = 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

              [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,
-            simps=SOME simps, inducts=SOME inducts, termination=termination }
+            simps=SOME simps, inducts=SOME inducts, termination=termination, cases=cases }
           in
             (info',
              lthy 
              |> Local_Theory.declaration {syntax = false, pervasive = false}
                (add_function_data o transform_function_data info')