src/HOL/BNF/Tools/bnf_fp_util.ML
changeset 52314 9606cf677021
parent 52312 f461dca57c66
child 52328 2f286a2b7f98
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu Jun 06 11:41:19 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu Jun 06 11:47:11 2013 +0200
     1.3 @@ -22,9 +22,9 @@
     1.4       dtor_ctors: thm list,
     1.5       ctor_dtors: thm list,
     1.6       ctor_injects: thm list,
     1.7 -     map_thms: thm list,
     1.8 -     set_thmss: thm list list,
     1.9 -     rel_thms: thm list,
    1.10 +     xtor_map_thms: thm list,
    1.11 +     xtor_set_thmss: thm list list,
    1.12 +     xtor_rel_thms: thm list,
    1.13       xtor_un_fold_thms: thm list,
    1.14       xtor_co_rec_thms: thm list}
    1.15  
    1.16 @@ -192,15 +192,15 @@
    1.17     dtor_ctors: thm list,
    1.18     ctor_dtors: thm list,
    1.19     ctor_injects: thm list,
    1.20 -   map_thms: thm list,
    1.21 -   set_thmss: thm list list,
    1.22 -   rel_thms: thm list,
    1.23 +   xtor_map_thms: thm list,
    1.24 +   xtor_set_thmss: thm list list,
    1.25 +   xtor_rel_thms: thm list,
    1.26     xtor_un_fold_thms: thm list,
    1.27     xtor_co_rec_thms: thm list};
    1.28  
    1.29  fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_un_folds, xtor_co_recs, xtor_co_induct,
    1.30 -    xtor_strong_co_induct, dtor_ctors, ctor_dtors, ctor_injects, map_thms, set_thmss, rel_thms,
    1.31 -    xtor_un_fold_thms, xtor_co_rec_thms} =
    1.32 +    xtor_strong_co_induct, dtor_ctors, ctor_dtors, ctor_injects, xtor_map_thms, xtor_set_thmss,
    1.33 +    xtor_rel_thms, xtor_un_fold_thms, xtor_co_rec_thms} =
    1.34    {Ts = map (Morphism.typ phi) Ts,
    1.35     bnfs = map (morph_bnf phi) bnfs,
    1.36     ctors = map (Morphism.term phi) ctors,
    1.37 @@ -212,9 +212,9 @@
    1.38     dtor_ctors = map (Morphism.thm phi) dtor_ctors,
    1.39     ctor_dtors = map (Morphism.thm phi) ctor_dtors,
    1.40     ctor_injects = map (Morphism.thm phi) ctor_injects,
    1.41 -   map_thms = map (Morphism.thm phi) map_thms,
    1.42 -   set_thmss = map (map (Morphism.thm phi)) set_thmss,
    1.43 -   rel_thms = map (Morphism.thm phi) rel_thms,
    1.44 +   xtor_map_thms = map (Morphism.thm phi) xtor_map_thms,
    1.45 +   xtor_set_thmss = map (map (Morphism.thm phi)) xtor_set_thmss,
    1.46 +   xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms,
    1.47     xtor_un_fold_thms = map (Morphism.thm phi) xtor_un_fold_thms,
    1.48     xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms};
    1.49