src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML

     eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
     etac notE THEN' atac ORELSE'
     (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt
        (@{thms id_def o_def split_def sum.cases} @ map_comps @ map_idents)))));
 
-fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse maybe_disc_fun sel_funs =
+fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse disc_fun_opt sel_funs =
   HEADGOAL (rtac ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN'
-    (the_default (K all_tac) (Option.map rtac maybe_disc_fun)) THEN' REPEAT_DETERM_N m o atac) THEN
+    (the_default (K all_tac) (Option.map rtac disc_fun_opt)) THEN' REPEAT_DETERM_N m o atac) THEN
   unfold_thms_tac ctxt (Let_def :: sel_funs) THEN HEADGOAL (rtac refl);
 
 fun inst_split_eq ctxt split =
   (case prop_of split of
     @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ (Var (_, Type (_, [T, _])) $ _) $ _) =>

   end;
 
 fun rulify_nchotomy n = funpow (n - 1) (fn thm => thm RS @{thm Meson.make_pos_rule'});
 
 fun mk_primcorec_raw_code_of_ctr_tac ctxt distincts discIs splits split_asms ms fun_ctrs
-    maybe_nchotomy =
+    nchotomy_opt =
   let
     val n = length ms;
     val (ms', fun_ctrs') =
-      (case maybe_nchotomy of
+      (case nchotomy_opt of
         NONE => (ms, fun_ctrs)
       | SOME nchotomy =>
         (ms |> split_last ||> K [n - 1] |> op @,
          fun_ctrs
          |> split_last