--- 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;