src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML

     val (_, tenv) = fo_match ctxt call pat;
   in
     (map0, Vartab.fold_rev (fn (_, (_, f)) => cons f) tenv [])
   end;
 
-fun dest_abs_or_applied_map_or_ctr _ _ (Abs (_, _, t)) = (Term.dummy, [t])
-  | dest_abs_or_applied_map_or_ctr ctxt s (t as t1 $ _) =
-    (case try (dest_map ctxt s) t1 of
-      SOME res => res
-    | NONE =>
-      let
-        val thy = Proof_Context.theory_of ctxt;
-        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_abs_or_applied_map_or_ctr"
-        else dest_map ctxt s (fst (dest_comb t'))
-      end);
+fun dest_abs_or_applied_map _ _ (Abs (_, _, t)) = (Term.dummy, [t])
+  | dest_abs_or_applied_map ctxt s (t1 $ _) = dest_map ctxt s t1;
 
 fun map_partition f xs =
   fold_rev (fn x => fn (ys, (good, bad)) =>
       case f x of SOME y => (y :: ys, (x :: good, bad)) | NONE => (ys, (good, x :: bad)))
     xs ([], ([], []));

          Type (s, map2 freeze_fpTs (flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) []
            (transpose callss)) Ts))
       and freeze_fpTs calls (T as Type (s, Ts)) =
           (case map_partition (try (snd o dest_map no_defs_lthy s)) calls of
             ([], _) =>
-            (case map_partition (try (snd o dest_abs_or_applied_map_or_ctr no_defs_lthy s)) calls of
+            (case map_partition (try (snd o dest_abs_or_applied_map no_defs_lthy s)) calls of
               ([], _) => freeze_fpTs_simple T
             | callsp => freeze_fpTs_map callsp s Ts)
           | callsp => freeze_fpTs_map callsp s Ts)
         | freeze_fpTs _ T = T;