compile

--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Sep 09 20:51:36 2014 +0200
@@ -411,7 +411,8 @@
           common_co_inducts = common_coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy) =
       nested_to_mutual_fps Greatest_FP bs res_Ts callers callssss0 lthy0;
 
-    val coinduct_attrs_pair = (case gfp_sugar_thms of SOME ((_, _, pair), _) => pair | NONE => []);
+    val coinduct_attrs_pair =
+      (case gfp_sugar_thms of SOME ((_, attrs_pair), _, _, _, _) => attrs_pair | NONE => ([], []));
 
     val perm_fp_sugars = sort (int_ord o pairself #fp_res_index) fp_sugars;
 
@@ -1412,7 +1413,7 @@
 
         val common_notes =
           [(coinductN, if n2m then [coinduct_thm] else [], common_coinduct_attrs),
-           (coinduct_strongN, if n2m then [coinduct_strong_thm] else [], common_coindut_attrs)]
+           (coinduct_strongN, if n2m then [coinduct_strong_thm] else [], common_coinduct_attrs)]
           |> filter_out (null o #2)
           |> map (fn (thmN, thms, attrs) =>
             ((Binding.qualify true common_name (Binding.name thmN), attrs), [(thms, [])]));