src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML

       in
         chop n disc_eqns ||> cons extra_disc_eqn |> (op @)
       end
   end;
 
-fun find_corec_calls ctxt has_call basic_ctr_specs ({ctr, sel, rhs_term, ...} : coeqn_data_sel) =
+fun find_corec_calls ctxt has_call (basic_ctr_specs : basic_corec_ctr_spec list)
+    ({ctr, sel, rhs_term, ...} : coeqn_data_sel) =
   let
     val sel_no = find_first (curry (op =) ctr o #ctr) basic_ctr_specs
       |> find_index (curry (op =) sel) o #sels o the;
     fun find t = if has_call t then snd (fold_rev_let_if_case ctxt (K cons) [] t []) else [];
   in

                 |> pair ctr
                 |> pair eqn_pos
                 |> single
             end;
 
-        fun prove_code exhaustive disc_eqns sel_eqns nchotomys ctr_alist ctr_specs =
+        fun prove_code exhaustive (disc_eqns : coeqn_data_disc list)
+            (sel_eqns : coeqn_data_sel list) nchotomys ctr_alist ctr_specs =
           let
             val fun_data_opt =
               (find_first (member (op =) (map #ctr ctr_specs) o #ctr) disc_eqns,
                find_first (member (op =) (map #ctr ctr_specs) o #ctr) sel_eqns)
               |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #code_rhs_opt x))

                       val ctr_thms =
                         map (the_default FalseE o AList.lookup (op =) ctr_alist o snd) cond_ctrs;
                     in SOME (false, rhs, raw_rhs, ctr_thms) end
                   | NONE =>
                     let
-                      fun prove_code_ctr {ctr, sels, ...} =
+                      fun prove_code_ctr ({ctr, sels, ...} : corec_ctr_spec) =
                         if not (exists (curry (op =) ctr o fst) ctr_alist) then NONE else
                           let
                             val prems = find_first (curry (op =) ctr o #ctr) disc_eqns
                               |> Option.map #prems |> the_default [];
                             val t =