--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Sun Feb 23 22:51:11 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Feb 24 00:04:48 2014 +0100
@@ -581,9 +581,10 @@
#> Binding.conceal
end;
- val ((bnfs, (deadss, livess)), (unfold_set, lthy)) = apfst (apsnd split_list o split_list)
- (fold_map2 (fn b => bnf_of_typ Smart_Inline (raw_qualify b) fp_sort Xs Ds0) bs rhsXs
- (empty_unfolds, lthy));
+ val ((bnfs, (deadss, livess)), ((_, unfold_set), lthy)) =
+ apfst (apsnd split_list o split_list)
+ (fold_map2 (fn b => bnf_of_typ Smart_Inline (raw_qualify b) fp_sort Xs Ds0) bs rhsXs
+ ((empty_comp_cache, empty_unfolds), lthy));
fun norm_qualify i = Binding.qualify true (Binding.name_of (nth bs (Int.max (0, i - 1))))
#> Binding.conceal;