1.1 --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Nov 04 10:52:41 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Nov 04 10:52:41 2013 +0100
     1.3 @@ -34,6 +34,20 @@
     1.4  
     1.5  val n2mN = "n2m_"
     1.6  
     1.7 +fun dest_applied_map_or_ctr ctxt s (t as t1 $ _) =
     1.8 +  (case try (dest_map ctxt s) t1 of
     1.9 +    SOME res => res
    1.10 +  | NONE =>
    1.11 +    let
    1.12 +      val thy = Proof_Context.theory_of ctxt;
    1.13 +      val map_thms = of_fp_sugar #mapss (the (fp_sugar_of ctxt s))
    1.14 +      val map_thms' = map (fn thm => thm RS sym RS eq_reflection) map_thms;
    1.15 +      val t' = Raw_Simplifier.rewrite_term thy map_thms' [] t;
    1.16 +    in
    1.17 +      if t aconv t' then raise Fail "dest_applied_map_or_ctr"
    1.18 +      else dest_map ctxt s (fst (dest_comb t'))
    1.19 +    end);
    1.20 +
    1.21  (* TODO: test with sort constraints on As *)
    1.22  (* TODO: use right sorting order for "fp_sort" w.r.t. original BNFs (?) -- treat new variables
    1.23     as deads? *)
    1.24 @@ -94,7 +108,7 @@
    1.25        and freeze_fp calls (T as Type (s, Ts)) =
    1.26            (case map_filter (try (snd o dest_map no_defs_lthy s)) calls of
    1.27              [] =>
    1.28 -            (case map_filter (try (snd o dest_map no_defs_lthy s o fst o dest_comb)) calls of
    1.29 +            (case map_filter (try (snd o dest_applied_map_or_ctr no_defs_lthy s)) calls of
    1.30                [] =>
    1.31                (case union (op = o pairself fst)
    1.32                    (maps (fn call => map (rpair call) (get_indices_checked call)) calls) [] of

     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Mon Nov 04 10:52:41 2013 +0100
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Mon Nov 04 10:52:41 2013 +0100
     2.3 @@ -802,19 +802,11 @@
     2.4        chop n disc_eqns ||> cons extra_disc_eqn |> (op @)
     2.5      end;
     2.6  
     2.7 -fun find_corec_calls has_call basic_ctr_specs {ctr, sel, rhs_term, ...} =
     2.8 +fun find_corec_calls has_call basic_ctr_specs ({ctr, sel, rhs_term, ...} : coeqn_data_sel) =
     2.9    let
    2.10      val sel_no = find_first (equal ctr o #ctr) basic_ctr_specs
    2.11        |> find_index (equal sel) o #sels o the;
    2.12 -    fun find (Abs (_, _, b)) = find b
    2.13 -      | find (t as _ $ _) =
    2.14 -        let val (f, args as arg :: _) = strip_comb t in
    2.15 -          if is_Free f andalso has_call f orelse is_Free arg andalso has_call arg then
    2.16 -            [t]
    2.17 -          else
    2.18 -            find f @ maps find args
    2.19 -        end
    2.20 -      | find f = if is_Free f andalso has_call f then [f] else [];
    2.21 +    fun find t = if has_call t then [t] else [];
    2.22    in
    2.23      find rhs_term
    2.24      |> K |> nth_map sel_no |> AList.map_entry (op =) ctr