# HG changeset patch
# User blanchet
# Date 1349082270 -7200
# Node ID 902b24e0ffb4818885aee42c83f862912f5c7868
# Parent  61729b1493972a692bf10a0fb3d5c1b2800cb29a
fixed recursor definition for datatypes with inner products (e.g. "'a trm" from the lambda-term example)

diff -r 61729b149397 -r 902b24e0ffb4 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Oct 01 10:46:30 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Oct 01 11:04:30 2012 +0200
@@ -604,8 +604,8 @@
                   if s = s' then build_map (build_ctor_rec_arg mk_proj) T U else mk_proj T
                 | _ => mk_proj T);
 
-            fun mk_U proj (T as Type (@{type_name prod}, [T', U])) =
-                if member (op =) fpTs T' then proj (T', U) else T
+            fun mk_U proj (Type (s as @{type_name prod}, Ts as [T', U])) =
+                if member (op =) fpTs T' then proj (T', U) else Type (s, map (mk_U proj) Ts)
               | mk_U proj (Type (s, Ts)) = Type (s, map (mk_U proj) Ts)
               | mk_U _ T = T;
 
diff -r 61729b149397 -r 902b24e0ffb4 src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Mon Oct 01 10:46:30 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Mon Oct 01 11:04:30 2012 +0200
@@ -100,7 +100,7 @@
 
 (*TODO: Try "sum_prod_thms_map" here, enriched with a few theorems*)
 val rec_like_unfold_thms =
-  @{thms comp_def convol_def fst_conv id_def map_pair_def prod_case_Pair_iden snd_conv split_conv
+  @{thms comp_def convol_def fst_conv id_def map_pair_simp prod_case_Pair_iden snd_conv split_conv
       sum.simps(5,6) sum_map.simps unit_case_Unity};
 
 fun mk_rec_like_tac pre_map_defs map_comp's map_ids'' rec_like_defs ctor_rec_like ctr_def ctxt =