# HG changeset patch
# User blanchet
# Date 1383666430 -3600
# Node ID 113990e513fbe92d364df88a3906600d4267e2ed
# Parent  7405328f4c3c5b9310dab94f3f2a3c6be413607e
tuning

diff -r 7405328f4c3c -r 113990e513fb src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Tue Nov 05 16:47:10 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Tue Nov 05 16:47:10 2013 +0100
@@ -472,7 +472,6 @@
       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;
@@ -482,8 +481,10 @@
         | 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,
@@ -739,7 +740,7 @@
           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)