1.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Wed Nov 06 10:35:30 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Wed Nov 06 12:01:48 2013 +0100
     1.3 @@ -97,20 +97,8 @@
     1.4      (map0, Vartab.fold_rev (fn (_, (_, f)) => cons f) tenv [])
     1.5    end;
     1.6  
     1.7 -fun dest_abs_or_applied_map_or_ctr _ _ (Abs (_, _, t)) = (Term.dummy, [t])
     1.8 -  | dest_abs_or_applied_map_or_ctr ctxt s (t as t1 $ _) =
     1.9 -    (case try (dest_map ctxt s) t1 of
    1.10 -      SOME res => res
    1.11 -    | NONE =>
    1.12 -      let
    1.13 -        val thy = Proof_Context.theory_of ctxt;
    1.14 -        val map_thms = flat (#mapss (the (fp_sugar_of ctxt s)));
    1.15 -        val map_thms' = map (fn thm => thm RS sym RS eq_reflection) map_thms;
    1.16 -        val t' = Raw_Simplifier.rewrite_term thy map_thms' [] t;
    1.17 -      in
    1.18 -        if t aconv t' then raise Fail "dest_abs_or_applied_map_or_ctr"
    1.19 -        else dest_map ctxt s (fst (dest_comb t'))
    1.20 -      end);
    1.21 +fun dest_abs_or_applied_map _ _ (Abs (_, _, t)) = (Term.dummy, [t])
    1.22 +  | dest_abs_or_applied_map ctxt s (t1 $ _) = dest_map ctxt s t1;
    1.23  
    1.24  fun map_partition f xs =
    1.25    fold_rev (fn x => fn (ys, (good, bad)) =>
    1.26 @@ -179,7 +167,7 @@
    1.27        and freeze_fpTs calls (T as Type (s, Ts)) =
    1.28            (case map_partition (try (snd o dest_map no_defs_lthy s)) calls of
    1.29              ([], _) =>
    1.30 -            (case map_partition (try (snd o dest_abs_or_applied_map_or_ctr no_defs_lthy s)) calls of
    1.31 +            (case map_partition (try (snd o dest_abs_or_applied_map no_defs_lthy s)) calls of
    1.32                ([], _) => freeze_fpTs_simple T
    1.33              | callsp => freeze_fpTs_map callsp s Ts)
    1.34            | callsp => freeze_fpTs_map callsp s Ts)