# HG changeset patch # User wenzelm # Date 1353181137 -3600 # Node ID 11cd86c5af3a7fdefe245a52280f289cf6a8fc50 # Parent 9e04e6edc5e768bfbd309666b632012e6e9241db tuned -- eliminate pointless ML method definition; diff -r 9e04e6edc5e7 -r 11cd86c5af3a src/Provers/classical.ML --- a/src/Provers/classical.ML Sat Nov 17 20:29:17 2012 +0100 +++ b/src/Provers/classical.ML Sat Nov 17 20:38:57 2012 +0100 @@ -906,11 +906,6 @@ end; -(* contradiction method *) - -val contradiction = Method.rule [Data.not_elim, Drule.rotate_prems 1 Data.not_elim]; - - (* automatic methods *) val cla_modifiers = @@ -936,7 +931,8 @@ Method.setup @{binding rule} (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules))) "apply some intro/elim rule (potentially classical)" #> - Method.setup @{binding contradiction} (Scan.succeed (K contradiction)) + Method.setup @{binding contradiction} + (Scan.succeed (K (Method.rule [Data.not_elim, Drule.rotate_prems 1 Data.not_elim]))) "proof by contradiction" #> Method.setup @{binding clarify} (cla_method' (CHANGED_PROP oo clarify_tac)) "repeatedly apply safe steps" #>