| changeset 60122 | eb08fefd5c05 |
| parent 60117 | 2712f40d6309 |
| child 60642 | 48dd1cefb4ae |
--- 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