--- a/src/Provers/classical.ML Tue Dec 15 16:57:10 2015 +0100
+++ b/src/Provers/classical.ML Wed Dec 16 16:31:36 2015 +0100
@@ -190,7 +190,7 @@
(*Creates rules to eliminate ~A, from rules to introduce A*)
fun swapify intrs = intrs RLN (2, [Data.swap]);
-val swapped = Thm.rule_attribute (fn _ => fn th => th RSN (2, Data.swap));
+val swapped = Thm.rule_attribute [] (fn _ => fn th => th RSN (2, Data.swap));
(*Uses introduction rules in the normal way, or on negated assumptions,
trying rules in order. *)