1.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Mon Feb 17 22:54:38 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Tue Feb 18 01:11:25 2014 +0100
     1.3 @@ -132,7 +132,7 @@
     1.4        else
     1.5          ((fp_sugars0, (NONE, NONE)), lthy);
     1.6  
     1.7 -    val {co_inducts = [induct], ...} :: _ = fp_sugars;
     1.8 +    val {common_co_inducts = [induct], ...} :: _ = fp_sugars;
     1.9      val inducts = map (the_single o #co_inducts) fp_sugars;
    1.10  
    1.11      fun mk_dtyp [] (TFree a) = Datatype_Aux.DtTFree a