src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML

     ((is_some gfp_sugar_thms, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
       co_induct_of coinduct_thms, strong_co_induct_of coinduct_thms, co_induct_of coinduct_thmss,
       strong_co_induct_of coinduct_thmss), lthy')
   end;
 
-val const_name = try (fn Const (v, _) => v);
 val undef_const = Const (@{const_name undefined}, dummyT);
 
 val abs_tuple = HOLogic.tupled_lambda o HOLogic.mk_tuple;
 fun abstract vs =
   let fun a n (t $ u) = a n t $ a n u
         | a n (Abs (v, T, b)) = Abs (v, T, a (n + 1) b)
         | a n t = let val idx = find_index (equal t) vs in
             if idx < 0 then t else Bound (n + idx) end
   in a 0 end;
-fun mk_prod1 Ts (t, u) = HOLogic.pair_const (fastype_of1 (Ts, t)) (fastype_of1 (Ts, u)) $ t $ u;
-fun mk_tuple1 Ts = the_default HOLogic.unit o try (foldr1 (mk_prod1 Ts));
+
+fun mk_prod1 bound_Ts (t, u) =
+  HOLogic.pair_const (fastype_of1 (bound_Ts, t)) (fastype_of1 (bound_Ts, u)) $ t $ u;
+fun mk_tuple1 bound_Ts = the_default HOLogic.unit o try (foldr1 (mk_prod1 bound_Ts));
 
 type coeqn_data_disc = {
   fun_name: string,
   fun_T: typ,
   fun_args: term list,

       fun rewrite bound_Ts U T (Abs (v, V, b)) = Abs (v, V, rewrite (V :: bound_Ts) U T b)
         | rewrite bound_Ts U T (t as _ $ _) =
           let val (u, vs) = strip_comb t in
             if is_Free u andalso has_call u then
               Inr_const U T $ mk_tuple1 bound_Ts vs
-            else if const_name u = SOME @{const_name prod_case} then
+            else if try (fst o dest_Const) u = SOME @{const_name prod_case} then
               map (rewrite bound_Ts U T) vs |> chop 1 |>> HOLogic.mk_split o the_single |> list_comb
             else
               list_comb (rewrite bound_Ts U T u, map (rewrite bound_Ts U T) vs)
           end
         | rewrite _ U T t =