# HG changeset patch
# User wenzelm
# Date 1429290102 -7200
# Node ID eb08fefd5c0563ce0c694cf4e614b6ba2a6c2a6b
# Parent  fd66c0f65c2329abf36dc43b627bd2171d921ef0
make SML/NJ happy;

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