# HG changeset patch
# User wenzelm
# Date 1429218093 -7200
# Node ID 820e8e704ba6ceac70955fe2084ba88a109668d0
# Parent  f5c4b49c8c9a36f74187bac245d479eb588c4e0e
make SML/NJ happy;

diff -r f5c4b49c8c9a -r 820e8e704ba6 src/HOL/Library/rewrite.ML
--- a/src/HOL/Library/rewrite.ML	Thu Apr 16 20:54:01 2015 +0200
+++ b/src/HOL/Library/rewrite.ML	Thu Apr 16 23:01:33 2015 +0200
@@ -130,8 +130,8 @@
 
 in
 
-val ft_arg = ft_arg_gen arg_rewr_cconv
-val ft_imp = ft_arg_gen imp_rewr_cconv
+fun ft_arg ctxt = ft_arg_gen arg_rewr_cconv ctxt
+fun ft_imp ctxt = ft_arg_gen imp_rewr_cconv ctxt
 
 end