src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 57397 5004aca20821
parent 57303 498a62e65f5f
child 57527 1b07ca054327
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Fri Jun 27 10:11:44 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Fri Jun 27 10:11:44 2014 +0200
     1.3 @@ -71,9 +71,10 @@
     1.4      val fp_absT_infos = map #absT_info fp_sugars;
     1.5      val fp_bnfs = of_fp_res #bnfs;
     1.6      val pre_bnfs = map #pre_bnf fp_sugars;
     1.7 -    val nesty_bnfss = map (fn sugar => #nested_bnfs sugar @ #nesting_bnfs sugar) fp_sugars;
     1.8 -    val fp_nesty_bnfss = fp_bnfs :: nesty_bnfss;
     1.9 -    val fp_nesty_bnfs = distinct (op = o pairself T_of_bnf) (flat fp_nesty_bnfss);
    1.10 +    val nesting_bnfss =
    1.11 +      map (fn sugar => #fp_nesting_bnfs sugar @ #live_nesting_bnfs sugar) fp_sugars;
    1.12 +    val fp_or_nesting_bnfss = fp_bnfs :: nesting_bnfss;
    1.13 +    val fp_or_nesting_bnfs = distinct (op = o pairself T_of_bnf) (flat fp_or_nesting_bnfss);
    1.14  
    1.15      val fp_absTs = map #absT fp_absT_infos;
    1.16      val fp_repTs = map #repT fp_absT_infos;
    1.17 @@ -137,7 +138,7 @@
    1.18  
    1.19      val rels =
    1.20        let
    1.21 -        fun find_rel T As Bs = fp_nesty_bnfss
    1.22 +        fun find_rel T As Bs = fp_or_nesting_bnfss
    1.23            |> map (filter_out (curry (op = o pairself name_of_bnf) BNF_Comp.DEADID_bnf))
    1.24            |> get_first (find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T)))
    1.25            |> Option.map (fn bnf =>
    1.26 @@ -186,7 +187,7 @@
    1.27          xtor's (mk_rel_xtor_co_induct_tactic fp abs_inverses rel_xtor_co_inducts rel_defs rel_monos)
    1.28          lthy;
    1.29  
    1.30 -    val rel_eqs = no_refl (map rel_eq_of_bnf fp_nesty_bnfs);
    1.31 +    val rel_eqs = no_refl (map rel_eq_of_bnf fp_or_nesting_bnfs);
    1.32      val map_id0s = no_refl (map map_id0_of_bnf bnfs);
    1.33  
    1.34      val xtor_co_induct_thm =
    1.35 @@ -419,7 +420,8 @@
    1.36  
    1.37          val map_thms = no_refl (maps (fn bnf =>
    1.38             let val map_comp0 = map_comp0_of_bnf bnf RS sym
    1.39 -           in [map_comp0, map_comp0 RS rewrite_comp_comp, map_id0_of_bnf bnf] end) fp_nesty_bnfs) @
    1.40 +           in [map_comp0, map_comp0 RS rewrite_comp_comp, map_id0_of_bnf bnf] end)
    1.41 +          fp_or_nesting_bnfs) @
    1.42            remove eq_thm_prop_untyped (case_fp fp @{thm comp_assoc[symmetric]} @{thm comp_assoc})
    1.43            (map2 (fn thm => fn bnf =>
    1.44              @{thm type_copy_map_comp0_undo} OF