1.1 --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Tue Nov 05 16:47:10 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Tue Nov 05 16:47:10 2013 +0100
     1.3 @@ -472,7 +472,6 @@
     1.4        strong_co_induct_of coinduct_thmss), lthy')
     1.5    end;
     1.6  
     1.7 -val const_name = try (fn Const (v, _) => v);
     1.8  val undef_const = Const (@{const_name undefined}, dummyT);
     1.9  
    1.10  val abs_tuple = HOLogic.tupled_lambda o HOLogic.mk_tuple;
    1.11 @@ -482,8 +481,10 @@
    1.12          | a n t = let val idx = find_index (equal t) vs in
    1.13              if idx < 0 then t else Bound (n + idx) end
    1.14    in a 0 end;
    1.15 -fun mk_prod1 Ts (t, u) = HOLogic.pair_const (fastype_of1 (Ts, t)) (fastype_of1 (Ts, u)) $ t $ u;
    1.16 -fun mk_tuple1 Ts = the_default HOLogic.unit o try (foldr1 (mk_prod1 Ts));
    1.17 +
    1.18 +fun mk_prod1 bound_Ts (t, u) =
    1.19 +  HOLogic.pair_const (fastype_of1 (bound_Ts, t)) (fastype_of1 (bound_Ts, u)) $ t $ u;
    1.20 +fun mk_tuple1 bound_Ts = the_default HOLogic.unit o try (foldr1 (mk_prod1 bound_Ts));
    1.21  
    1.22  type coeqn_data_disc = {
    1.23    fun_name: string,
    1.24 @@ -739,7 +740,7 @@
    1.25            let val (u, vs) = strip_comb t in
    1.26              if is_Free u andalso has_call u then
    1.27                Inr_const U T $ mk_tuple1 bound_Ts vs
    1.28 -            else if const_name u = SOME @{const_name prod_case} then
    1.29 +            else if try (fst o dest_Const) u = SOME @{const_name prod_case} then
    1.30                map (rewrite bound_Ts U T) vs |> chop 1 |>> HOLogic.mk_split o the_single |> list_comb
    1.31              else
    1.32                list_comb (rewrite bound_Ts U T u, map (rewrite bound_Ts U T) vs)