diff -r fd66c0f65c23 -r eb08fefd5c05 src/HOL/Library/rewrite.ML
--- a/src/HOL/Library/rewrite.ML	Fri Apr 17 18:02:32 2015 +0200
+++ b/src/HOL/Library/rewrite.ML	Fri Apr 17 19:01:42 2015 +0200
@@ -152,8 +152,8 @@
 
 in
 
-val arg_pconv = arg_pconv_gen CConv.arg_cconv
-val imp_pconv = arg_pconv_gen (CConv.concl_cconv 1)
+fun arg_pconv ctxt = arg_pconv_gen CConv.arg_cconv ctxt
+fun imp_pconv ctxt = arg_pconv_gen (CConv.concl_cconv 1) ctxt
 
 end