1.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Nov 04 14:54:29 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Nov 04 15:44:43 2013 +0100
     1.3 @@ -88,16 +88,25 @@
     1.4          else dest_map ctxt s (fst (dest_comb t'))
     1.5        end);
     1.6  
     1.7 +fun map_partition f xs =
     1.8 +  fold_rev (fn x => fn (ys, (good, bad)) =>
     1.9 +      case f x of SOME y => (y :: ys, (x :: good, bad)) | NONE => (ys, (good, x :: bad)))
    1.10 +    xs ([], ([], []));
    1.11 +
    1.12  (* TODO: test with sort constraints on As *)
    1.13  (* TODO: use right sorting order for "fp_sort" w.r.t. original BNFs (?) -- treat new variables
    1.14     as deads? *)
    1.15 -fun mutualize_fp_sugars has_nested fp bs fpTs _ callssss fp_sugars0 no_defs_lthy0 =
    1.16 +fun mutualize_fp_sugars has_nested fp bs fpTs get_indices callssss fp_sugars0 no_defs_lthy0 =
    1.17    if has_nested orelse has_duplicates (op =) fpTs then
    1.18      let
    1.19        val thy = Proof_Context.theory_of no_defs_lthy0;
    1.20  
    1.21        val qsotm = quote o Syntax.string_of_term no_defs_lthy0;
    1.22  
    1.23 +      fun incompatible_calls t1 t2 =
    1.24 +        error ("Incompatible " ^ co_prefix fp ^ "recursive calls: " ^ qsotm t1 ^ " vs. " ^
    1.25 +          qsotm t2);
    1.26 +
    1.27        val b_names = map Binding.name_of bs;
    1.28        val fp_b_names = map base_name_of_typ fpTs;
    1.29  
    1.30 @@ -133,16 +142,20 @@
    1.31            | kk => nth Xs kk)
    1.32          | freeze_fp_default T = T;
    1.33  
    1.34 -      fun freeze_fp_map callss s Ts =
    1.35 -        Type (s, map2 freeze_fp (flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) []
    1.36 -          (transpose callss)) Ts)
    1.37 +      fun check_call_dead live_call call =
    1.38 +        if null (get_indices call) then () else incompatible_calls live_call call;
    1.39 +
    1.40 +      fun freeze_fp_map (callss, (live_call :: _, dead_calls)) s Ts =
    1.41 +        (List.app (check_call_dead live_call) dead_calls;
    1.42 +         Type (s, map2 freeze_fp (flatten_type_args_of_bnf (the (bnf_of no_defs_lthy s)) []
    1.43 +           (transpose callss)) Ts))
    1.44        and freeze_fp calls (T as Type (s, Ts)) =
    1.45 -          (case map_filter (try (snd o dest_map no_defs_lthy s)) calls of
    1.46 -            [] =>
    1.47 -            (case map_filter (try (snd o dest_abs_or_applied_map_or_ctr no_defs_lthy s)) calls of
    1.48 -              [] => freeze_fp_default T
    1.49 -            | callss => freeze_fp_map callss s Ts)
    1.50 -          | callss => freeze_fp_map callss s Ts)
    1.51 +          (case map_partition (try (snd o dest_map no_defs_lthy s)) calls of
    1.52 +            ([], _) =>
    1.53 +            (case map_partition (try (snd o dest_abs_or_applied_map_or_ctr no_defs_lthy s)) calls of
    1.54 +              ([], _) => freeze_fp_default T
    1.55 +            | callsp => freeze_fp_map callsp s Ts)
    1.56 +          | callsp => freeze_fp_map callsp s Ts)
    1.57          | freeze_fp _ T = T;
    1.58  
    1.59        val ctr_Tsss = map (map binder_types) ctr_Tss;