diff -r 4bee6d8c1500 -r 26bf09b95dda src/Tools/intuitionistic.ML --- 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));