--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Fri Sep 26 14:41:54 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Fri Sep 26 14:43:26 2014 +0200
@@ -297,9 +297,9 @@
val Xs' = map #X fp_sugars';
val ctrXs_Tsss' = map (map (map substAT) o #ctrXs_Tss o #fp_ctr_sugar) fp_sugars';
val ctrss' = map2 mk_ctr_of fp_sugars' fpTs';
- val {common_co_inducts = induct :: _, ...} :: _ = fp_sugars';
+ val {fp_co_induct_sugar = {common_co_inducts = induct :: _, ...}, ...} :: _ = fp_sugars';
val inducts = map (hd o #co_inducts o #fp_co_induct_sugar) fp_sugars';
- val recs = map #co_rec fp_sugars';
+ val recs = map (#co_rec o #fp_co_induct_sugar) fp_sugars';
val rec_thmss = map (#co_rec_thms o #fp_co_induct_sugar) fp_sugars';
fun is_nested_rec_type (Type (@{type_name fun}, [_, T])) = member (op =) Xs' (body_type T)