# HG changeset patch # User blanchet # Date 1410454476 -7200 # Node ID de95aeedf49e6248ae6c5c96717122c302ed13b1 # Parent 055afb5f7df81447873126a14c11dce9f14d78b0 fixed situation in 'primrec' whereby the original value of a constructor argument of nested type was not translated correctly to a 'map fst' diff -r 055afb5f7df8 -r de95aeedf49e src/HOL/Library/RBT_Set.thy --- a/src/HOL/Library/RBT_Set.thy Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/Library/RBT_Set.thy Thu Sep 11 18:54:36 2014 +0200 @@ -10,7 +10,7 @@ (* Users should be aware that by including this file all code equations - outside of List.thy using 'a list as an implenentation of sets cannot be + outside of List.thy using 'a list as an implementation of sets cannot be used for code generation. If such equations are not needed, they can be deleted from the code generator. Otherwise, a user has to provide their own equations using RBT trees. diff -r 055afb5f7df8 -r de95aeedf49e src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Thu Sep 11 18:54:36 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Thu Sep 11 18:54:36 2014 +0200 @@ -296,25 +296,27 @@ fun subst bound_Ts (t as g' $ y) = let - fun subst_rec () = subst bound_Ts g' $ subst bound_Ts y; + fun subst_rec (h $ z) = subst bound_Ts h $ subst bound_Ts z + | subst_rec t = t; + val y_head = head_of y; in if not (member (op =) ctr_args y_head) then - subst_rec () + subst_rec t else (case try_nested_rec bound_Ts y_head t of - SOME t' => t' + SOME t' => subst_rec t' | NONE => let val (g, g_args) = strip_comb g' in (case try (get_ctr_pos o fst o dest_Free) g of - SOME ~1 => subst_rec () + SOME ~1 => subst_rec t | SOME ctr_pos => (length g_args >= ctr_pos orelse raise PRIMREC ("too few arguments in recursive call", [t]); (case AList.lookup (op =) mutual_calls y of SOME y' => list_comb (y', g_args) - | NONE => subst_rec ())) - | NONE => subst_rec ()) + | NONE => subst_rec t)) + | NONE => subst_rec t) end) end | subst bound_Ts (Abs (v, T, b)) = Abs (v, T, subst (T :: bound_Ts) b)