--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Wed Nov 06 10:35:30 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Wed Nov 06 12:01:48 2013 +0100
@@ -97,20 +97,8 @@
(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)) =>
@@ -179,7 +167,7 @@
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)