src/HOL/Tools/Quotient/quotient_def.ML

--- a/src/HOL/Tools/Quotient/quotient_def.ML	Fri Mar 06 14:01:08 2015 +0100
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Fri Mar 06 15:58:56 2015 +0100
@@ -91,7 +91,7 @@
 
 fun mk_readable_rsp_thm_eq tm lthy =
   let
-    val ctm = Proof_Context.cterm_of lthy tm
+    val ctm = Thm.cterm_of lthy tm
     
     fun norm_fun_eq ctm = 
       let