src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML
changeset 54239 9bd91d5d8a7b
parent 54235 3aed2ae6eb91
child 54240 756ff45e08ba
     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