src/Sequents/prover.ML
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);