--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Mon Nov 04 10:52:41 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Mon Nov 04 10:52:41 2013 +0100
@@ -34,6 +34,20 @@
val n2mN = "n2m_"
+fun dest_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 = of_fp_sugar #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"
+ else dest_map ctxt s (fst (dest_comb t'))
+ end);
+
(* TODO: test with sort constraints on As *)
(* TODO: use right sorting order for "fp_sort" w.r.t. original BNFs (?) -- treat new variables
as deads? *)
@@ -94,7 +108,7 @@
and freeze_fp calls (T as Type (s, Ts)) =
(case map_filter (try (snd o dest_map no_defs_lthy s)) calls of
[] =>
- (case map_filter (try (snd o dest_map no_defs_lthy s o fst o dest_comb)) calls of
+ (case map_filter (try (snd o dest_applied_map_or_ctr no_defs_lthy s)) calls of
[] =>
(case union (op = o pairself fst)
(maps (fn call => map (rpair call) (get_indices_checked call)) calls) [] of
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Mon Nov 04 10:52:41 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Mon Nov 04 10:52:41 2013 +0100
@@ -802,19 +802,11 @@
chop n disc_eqns ||> cons extra_disc_eqn |> (op @)
end;
-fun find_corec_calls has_call basic_ctr_specs {ctr, sel, rhs_term, ...} =
+fun find_corec_calls has_call basic_ctr_specs ({ctr, sel, rhs_term, ...} : coeqn_data_sel) =
let
val sel_no = find_first (equal ctr o #ctr) basic_ctr_specs
|> find_index (equal sel) o #sels o the;
- fun find (Abs (_, _, b)) = find b
- | find (t as _ $ _) =
- let val (f, args as arg :: _) = strip_comb t in
- if is_Free f andalso has_call f orelse is_Free arg andalso has_call arg then
- [t]
- else
- find f @ maps find args
- end
- | find f = if is_Free f andalso has_call f then [f] else [];
+ fun find t = if has_call t then [t] else [];
in
find rhs_term
|> K |> nth_map sel_no |> AList.map_entry (op =) ctr