changeset 58048 | aa6296d09e0e |
parent 57859 | 29e728588163 |
child 59498 | 50b60f501b05 |
--- a/src/Sequents/prover.ML Wed Aug 27 12:32:42 2014 +0200 +++ b/src/Sequents/prover.ML Wed Aug 27 14:54:32 2014 +0200 @@ -106,8 +106,8 @@ fun method tac = Method.sections - [Args.$$$ "add" -- Args.bang_colon >> K (I, safe_add), - Args.$$$ "add" -- Args.colon >> K (I, unsafe_add)] + [Args.$$$ "add" -- Args.bang_colon >> K (Method.modifier safe_add @{here}), + Args.$$$ "add" -- Args.colon >> K (Method.modifier unsafe_add @{here})] >> K (SIMPLE_METHOD' o tac);