| changeset 58963 | 26bf09b95dda |
| parent 58957 | c9e744ea8a38 |
| child 59164 | ff40c53d1af9 |
--- a/src/Tools/intuitionistic.ML Sun Nov 09 20:49:28 2014 +0100 +++ b/src/Tools/intuitionistic.ML Mon Nov 10 21:49:48 2014 +0100 @@ -34,7 +34,7 @@ fun unsafe_step_tac ctxt = Context_Rules.wrap ctxt - (assume_tac APPEND' + (assume_tac ctxt APPEND' bires_tac false (Context_Rules.netpair_bang ctxt) APPEND' bires_tac false (Context_Rules.netpair ctxt));