changeset 59580 | cbc38731d42f |
parent 59157 | 949829bae42a |
child 59582 | 0fbed69ff081 |
--- a/src/HOL/Tools/Quotient/quotient_def.ML Tue Mar 03 17:20:51 2015 +0100 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Tue Mar 03 19:08:04 2015 +0100 @@ -91,7 +91,7 @@ fun mk_readable_rsp_thm_eq tm lthy = let - val ctm = cterm_of (Proof_Context.theory_of lthy) tm + val ctm = Proof_Context.cterm_of lthy tm fun norm_fun_eq ctm = let