src/Provers/classical.ML
changeset 50112 11cd86c5af3a
parent 50108 f171b5240c31
child 51580 64ef8260dc60
--- 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" #>