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 (