changeset 30549 | d2d7874648bd |
parent 30510 | 4120fc59dd85 |
child 35762 | af3ff2ba4c54 |
--- a/src/Sequents/T.thy Mon Mar 16 17:51:24 2009 +0100 +++ b/src/Sequents/T.thy Mon Mar 16 18:24:30 2009 +0100 @@ -44,7 +44,7 @@ *} method_setup T_solve = - {* Method.no_args (SIMPLE_METHOD (T_Prover.solve_tac 2)) *} "T solver" + {* Scan.succeed (K (SIMPLE_METHOD (T_Prover.solve_tac 2))) *} "T solver" (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)