# HG changeset patch
# User blanchet
# Date 1383666430 -3600
# Node ID 7405328f4c3c5b9310dab94f3f2a3c6be413607e
# Parent  dcdfec41a3252e4179e47b7c0bb105fd4cadb8c3
get mutually recursive maps as well

diff -r dcdfec41a325 -r 7405328f4c3c src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Nov 05 15:10:59 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Tue Nov 05 16:47:10 2013 +0100
@@ -104,11 +104,11 @@
     | NONE =>
       let
         val thy = Proof_Context.theory_of ctxt;
-        val map_thms = of_fp_sugar #mapss (the (fp_sugar_of ctxt s))
+        val map_thms = flat (#mapss (the (fp_sugar_of ctxt s)));
         val map_thms' = map (fn thm => thm RS sym RS eq_reflection) map_thms;
         val t' = Raw_Simplifier.rewrite_term thy map_thms' [] t;
       in
-        if t aconv t' then raise Fail "dest_applied_map_or_ctr"
+        if t aconv t' then raise Fail "dest_abs_or_applied_map_or_ctr"
         else dest_map ctxt s (fst (dest_comb t'))
       end);