| changeset 54742 | 7a86358a3c0b |
| parent 51309 | 473303ef6e34 |
| child 60770 | 240563fbf41d |
--- a/src/Sequents/T.thy Fri Dec 13 23:53:02 2013 +0100 +++ b/src/Sequents/T.thy Sat Dec 14 17:28:05 2013 +0100 @@ -42,7 +42,7 @@ ) *} -method_setup T_solve = {* Scan.succeed (K (SIMPLE_METHOD (T_Prover.solve_tac 2))) *} +method_setup T_solve = {* Scan.succeed (fn ctxt => SIMPLE_METHOD (T_Prover.solve_tac ctxt 2)) *} (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)