Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 54740 91f54d386680
parent 54626 8a5e82425e55 
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Dec 13 14:58:47 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Dec 13 20:20:15 2013 +0100
@@ -156,7 +156,7 @@
    sel_co_iterssss = map (map (map (map (Morphism.thm phi)))) sel_co_iterssss};
 
 val transfer_fp_sugar =
-  morph_fp_sugar o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
+  morph_fp_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
 
 structure Data = Generic_Data
 (
@@ -344,7 +344,7 @@
    (map (map (Morphism.thm phi)) foldss, map (map (Morphism.thm phi)) recss, iter_attrs));
 
 val transfer_lfp_sugar_thms =
-  morph_lfp_sugar_thms o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
+  morph_lfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;
 
 type gfp_sugar_thms =
   ((thm list * thm) list * Args.src list)
@@ -368,7 +368,7 @@
     map (map (map (Morphism.thm phi))) sel_corecsss, sel_iter_attrs));
 
 val transfer_gfp_sugar_thms =
-  morph_gfp_sugar_thms o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
+  morph_gfp_sugar_thms o Morphism.transfer_morphism o Proof_Context.theory_of;
 
 fun mk_iter_fun_arg_types0 n ms = map2 dest_tupleT ms o dest_sumTN_balanced n o domain_type;
isabelle