author | kuncar |
Fri, 10 May 2013 19:41:23 +0200 | |
changeset 51927 | bcd6898ac613 |
parent 51926 | 25ceb5fa8f78 |
child 51928 | a5265222d6e6 |
child 51929 | 5e8a0b8bb070 |
--- a/src/HOL/Tools/Lifting/lifting_def.ML Fri May 10 06:34:29 2013 +0200 +++ b/src/HOL/Tools/Lifting/lifting_def.ML Fri May 10 19:41:23 2013 +0200 @@ -115,7 +115,6 @@ let val transfer_rule = ([quot_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer}) - |> Morphism.thm (Local_Theory.target_morphism lthy) |> Lifting_Term.parametrize_transfer_rule lthy in (option_fold transfer_rule (generate_parametric_transfer_rule lthy transfer_rule) opt_par_thm