# HG changeset patch
# User blanchet
# Date 1383558761 -3600
# Node ID 9bd91d5d8a7bc2c00af75144fff870788eca1e8e
# Parent  58742c75920570c688d9cd4080da5eeb17a5df2c
handle constructor syntax in n2m primcorec

diff -r 58742c759205 -r 9bd91d5d8a7b src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
--- 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
diff -r 58742c759205 -r 9bd91d5d8a7b src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- 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