| changeset 54742 | 7a86358a3c0b |
| parent 52143 | 36ffe23b25f8 |
| child 60770 | 240563fbf41d |
--- a/src/Sequents/S43.thy Fri Dec 13 23:53:02 2013 +0100 +++ b/src/Sequents/S43.thy Sat Dec 14 17:28:05 2013 +0100 @@ -90,8 +90,8 @@ method_setup S43_solve = {* - Scan.succeed (K (SIMPLE_METHOD - (S43_Prover.solve_tac 2 ORELSE S43_Prover.solve_tac 3))) + Scan.succeed (fn ctxt => SIMPLE_METHOD + (S43_Prover.solve_tac ctxt 2 ORELSE S43_Prover.solve_tac ctxt 3)) *}