src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 54740 91f54d386680
parent 54701 4ed7454aebde
child 54900 136fe16e726a
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Dec 13 14:58:47 2013 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Dec 13 20:20:15 2013 +0100
@@ -125,7 +125,7 @@
    case_eq_ifs = map (Morphism.thm phi) case_eq_ifs};
 
 val transfer_ctr_sugar =
-  morph_ctr_sugar o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of;
+  morph_ctr_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
 
 structure Data = Generic_Data
 (