# HG changeset patch
# User blanchet
# Date 1473150498 -7200
# Node ID 737d424cbac9a3eba85df187103acf7514e21025
# Parent  362160f9c68a2bc171110ba27316acfd63f89146
generalized code (subtly)

diff -r 362160f9c68a -r 737d424cbac9 src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Tue Sep 06 10:09:33 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Tue Sep 06 10:28:18 2016 +0200
@@ -930,8 +930,6 @@
     val time = time lthy;
     val timer = time (Timer.startRealTimer ());
 
-    val nn = length Xs;
-
     fun flatten_tyargs Ass =
       subtract (op =) Xs (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs) @ Xs;
 
@@ -966,7 +964,7 @@
 
     val ((pre_bnfs, (deadss, absT_infos)), lthy''') =
       @{fold_map 4} (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b))
-        bs (not (null live_phantoms) :: replicate (nn - 1) false) Dss bnfs' lthy''
+        bs (not (null live_phantoms) :: replicate (length rhsXs - 1) false) Dss bnfs' lthy''
       |>> split_list
       |>> apsnd split_list;