src/HOL/Library/rewrite.ML
changeset 60109 22389d4cdd6b
parent 60108 d7fe3e0aca85
parent 60102 820e8e704ba6
child 60117 2712f40d6309
     1.1 --- a/src/HOL/Library/rewrite.ML	Fri Apr 17 10:49:57 2015 +0200
     1.2 +++ b/src/HOL/Library/rewrite.ML	Fri Apr 17 11:12:19 2015 +0200
     1.3 @@ -130,8 +130,8 @@
     1.4  
     1.5  in
     1.6  
     1.7 -val ft_arg = ft_arg_gen arg_rewr_cconv
     1.8 -val ft_imp = ft_arg_gen imp_rewr_cconv
     1.9 +fun ft_arg ctxt = ft_arg_gen arg_rewr_cconv ctxt
    1.10 +fun ft_imp ctxt = ft_arg_gen imp_rewr_cconv ctxt
    1.11  
    1.12  end
    1.13