| changeset 60109 | 22389d4cdd6b |
| parent 60108 | d7fe3e0aca85 |
| parent 60102 | 820e8e704ba6 |
| child 60117 | 2712f40d6309 |
--- a/src/HOL/Library/rewrite.ML Fri Apr 17 10:49:57 2015 +0200 +++ b/src/HOL/Library/rewrite.ML Fri Apr 17 11:12:19 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