src/HOL/Tools/Function/mutual.ML

   end
 
 fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof =
   let
     val result = inner_cont proof
-    val FunctionResult {G, R, cases, psimps, trsimps, simple_pinducts=[simple_pinduct],
+    val FunctionResult {G, R, cases, psimps, simple_pinducts=[simple_pinduct],
       termination, domintros, ...} = result
 
     val (all_f_defs, fs) =
       map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} =>
         (mk_applied_form lthy cargTs (Thm.symmetric f_def), f))

     fun mk_mpsimp fqgar sum_psimp =
       in_context lthy fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp
 
     val rew_ss = HOL_basic_ss addsimps all_f_defs
     val mpsimps = map2 mk_mpsimp fqgars psimps
-    val mtrsimps = Option.map (map2 mk_mpsimp fqgars) trsimps
     val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m
     val mtermination = full_simplify rew_ss termination
     val mdomintros = Option.map (map (full_simplify rew_ss)) domintros
   in
     FunctionResult { fs=fs, G=G, R=R,
       psimps=mpsimps, simple_pinducts=minducts,
       cases=cases, termination=mtermination,
-      domintros=mdomintros, trsimps=mtrsimps}
+      domintros=mdomintros}
   end
 
 fun prepare_function_mutual config defname fixes eqss lthy =
   let
     val mutual as Mutual {fsum_var=(n, T), qglrs, ...} =