1.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Nov 05 15:10:59 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Nov 05 16:47:10 2013 +0100
     1.3 @@ -104,11 +104,11 @@
     1.4      | NONE =>
     1.5        let
     1.6          val thy = Proof_Context.theory_of ctxt;
     1.7 -        val map_thms = of_fp_sugar #mapss (the (fp_sugar_of ctxt s))
     1.8 +        val map_thms = flat (#mapss (the (fp_sugar_of ctxt s)));
     1.9          val map_thms' = map (fn thm => thm RS sym RS eq_reflection) map_thms;
    1.10          val t' = Raw_Simplifier.rewrite_term thy map_thms' [] t;
    1.11        in
    1.12 -        if t aconv t' then raise Fail "dest_applied_map_or_ctr"
    1.13 +        if t aconv t' then raise Fail "dest_abs_or_applied_map_or_ctr"
    1.14          else dest_map ctxt s (fst (dest_comb t'))
    1.15        end);
    1.16