changeset 30510 | 4120fc59dd85 |
parent 30165 | 6ee87f67d9cd |
child 31299 | 0c5baf034d0e |
--- a/src/Tools/intuitionistic.ML Fri Mar 13 19:53:09 2009 +0100 +++ b/src/Tools/intuitionistic.ML Fri Mar 13 19:58:26 2009 +0100 @@ -86,7 +86,7 @@ val method = Method.bang_sectioned_args' modifiers (Scan.lift (Scan.option OuterParse.nat)) - (fn n => fn prems => fn ctxt => Method.METHOD (fn facts => + (fn n => fn prems => fn ctxt => METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt n)));