src/Sequents/T.thy
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 *)