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