# HG changeset patch
# User blanchet
# Date 1383558761 -3600
# Node ID b5310a1b807c14d25746ac7235223c15119e75ab
# Parent  6d64669184ae6dbbe0d8cba126aa038d6a72a4c0
make code more robust w.r.t. applied/unapplied map (primrec vs. primcorec)

diff -r 6d64669184ae -r b5310a1b807c 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
@@ -88,17 +88,21 @@
           _ :: _ :: _ => heterogeneous_call call
         | kks => kks);
 
-      fun freeze_fp calls (T as Type (s, Ts)) =
+      fun freeze_fp_map callss s Ts =
+        Type (s, map2 freeze_fp (flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) []
+          (transpose callss)) Ts)
+      and freeze_fp calls (T as Type (s, Ts)) =
           (case map_filter (try (snd o dest_map no_defs_lthy s)) calls of
             [] =>
-            (case union (op = o pairself fst)
-                (maps (fn call => map (rpair call) (get_indices_checked call)) calls) [] of
-              [] => freeze_fp_default T
-            | [(kk, _)] => nth Xs kk
-            | (_, call1) :: (_, call2) :: _ => incompatible_calls call1 call2)
-          | callss =>
-            Type (s, map2 freeze_fp (flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) []
-              (transpose callss)) Ts))
+            (case map_filter (try (snd o dest_map no_defs_lthy s o fst o dest_comb)) calls of
+              [] =>
+              (case union (op = o pairself fst)
+                  (maps (fn call => map (rpair call) (get_indices_checked call)) calls) [] of
+                [] => freeze_fp_default T
+              | [(kk, _)] => nth Xs kk
+              | (_, call1) :: (_, call2) :: _ => incompatible_calls call1 call2)
+            | callss => freeze_fp_map callss s Ts)
+          | callss => freeze_fp_map callss s Ts)
         | freeze_fp _ T = T;
 
       val ctr_Tsss = map (map binder_types) ctr_Tss;