# 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" #>