--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Sep 26 14:43:26 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Sep 26 14:43:28 2014 +0200
@@ -400,7 +400,7 @@
| _ => not_codatatype ctxt res_T);
fun map_thms_of_typ ctxt (Type (s, _)) =
- (case fp_sugar_of ctxt s of SOME {maps, ...} => maps | NONE => [])
+ (case fp_sugar_of ctxt s of SOME {fp_bnf_sugar = {map_thms, ...}, ...} => map_thms | NONE => [])
| map_thms_of_typ _ _ = [];
fun corec_specs_of bs arg_Ts res_Ts callers callssss0 lthy0 =