src/HOL/Tools/Function/function.ML

             ||> (snd o Local_Theory.note ((qualify "cases",
                    [Attrib.internal (K (Rule_Cases.case_names cnames))]), [cases]))
             ||> fold_option (snd oo curry Local_Theory.note (qualify "domintros", [])) domintros
 
           val info = { add_simps=addsmps, case_names=cnames, psimps=psimps',
-            pinducts=snd pinducts', termination=termination', fs=fs, R=R,
-            defname=defname, is_partial=true }
+            pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
+            fs=fs, R=R, defname=defname, is_partial=true }
 
           val _ =
             if not is_external then ()
             else Specification.print_consts lthy (K false) (map fst fixes)
         in

             val remove_domain_condition =
               full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
             val tsimps = map remove_domain_condition psimps
             val tinduct = map remove_domain_condition pinducts
 
-            val info' = { is_partial=false, defname=defname, add_simps=add_simps,
-              case_names=case_names, fs=fs, R=R, psimps=psimps, pinducts=pinducts,
-              termination=termination }
             fun qualify n = Binding.name n
               |> Binding.qualify true defname
           in
             lthy
-            |> add_simps I "simps" I simp_attribs tsimps |> snd
-            |> Local_Theory.note
+            |> add_simps I "simps" I simp_attribs tsimps
+            ||>> Local_Theory.note
                ((qualify "induct",
                  [Attrib.internal (K (Rule_Cases.case_names case_names))]),
-                tinduct) |> snd
-            |> Local_Theory.declaration false (add_function_data o morph_function_data info')
+                tinduct)
+            |-> (fn (simps, (_, inducts)) =>
+              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 }
+              in
+                Local_Theory.declaration false (add_function_data o morph_function_data info')
+              end)
           end
     in
       lthy
       |> ProofContext.note_thmss ""
          [((Binding.empty, [Context_Rules.rule_del]), [([allI], [])])] |> snd