# HG changeset patch
# User blanchet
# Date 1383559393 -3600
# Node ID 756ff45e08ba466345fc0a8ce2d146e1a57683f4
# Parent  9bd91d5d8a7bc2c00af75144fff870788eca1e8e
made n2m code more robust w.r.t. advanced constructs (e.g. lambdas)

diff -r 9bd91d5d8a7b -r 756ff45e08ba 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 11:03:13 2013 +0100
@@ -58,10 +58,6 @@
 
       val qsotm = quote o Syntax.string_of_term no_defs_lthy0;
 
-      fun heterogeneous_call t = error ("Heterogeneous recursive call: " ^ qsotm t);
-      fun incompatible_calls t1 t2 =
-        error ("Incompatible recursive calls: " ^ qsotm t1 ^ " vs. " ^ qsotm t2);
-
       val b_names = map Binding.name_of bs;
       val fp_b_names = map base_name_of_typ fpTs;
 
@@ -97,11 +93,6 @@
           | kk => nth Xs kk)
         | freeze_fp_default T = T;
 
-      fun get_indices_checked call =
-        (case get_indices call of
-          _ :: _ :: _ => heterogeneous_call call
-        | kks => kks);
-
       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)
@@ -109,12 +100,7 @@
           (case map_filter (try (snd o dest_map no_defs_lthy s)) 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
-                [] => freeze_fp_default T
-              | [(kk, _)] => nth Xs kk
-              | (_, call1) :: (_, call2) :: _ => incompatible_calls call1 call2)
+              [] => freeze_fp_default T
             | callss => freeze_fp_map callss s Ts)
           | callss => freeze_fp_map callss s Ts)
         | freeze_fp _ T = T;