src/HOL/Tools/Function/function.ML

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

         val (((psimps', pinducts'), (_, [termination'])), lthy) =
           lthy
           |> addsmps (conceal_partial o Binding.qualify false "partial")
                "psimps" conceal_partial psimp_attribs psimps
           ||> fold_option (snd oo addsmps I "simps" I simp_attribs) trsimps
-          ||> fold_option (Spec_Rules.add Spec_Rules.Equational o (pair fs)) trsimps
+          ||> fold_option (Spec_Rules.add Spec_Rules.Equational o pair fs) trsimps
           ||>> Local_Theory.note ((conceal_partial (qualify "pinduct"),
                  [Attrib.internal (K (Rule_Cases.case_names cnames)),
                   Attrib.internal (K (Rule_Cases.consumes 1)),
                   Attrib.internal (K (Induct.induct_pred ""))]), simple_pinducts)
           ||>> Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination])

             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')
-              #> Spec_Rules.add Spec_Rules.Equational (fs, simps)
+              #> Spec_Rules.add Spec_Rules.Equational (fs, tsimps)
             end)
         end
   in
     lthy
     |> ProofContext.note_thmss ""