# HG changeset patch
# User wenzelm
# Date 1435671671 -7200
# Node ID 7512716f03dbe10806053be59ea99249c1557aa0
# Parent  4c79543cc376e047f601ba9bedaa53e8e8ead3ed
no arguments for "standard" (or old "default") methods;

diff -r 4c79543cc376 -r 7512716f03db src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue Jun 30 15:20:56 2015 +0200
+++ b/src/Provers/classical.ML	Tue Jun 30 15:41:11 2015 +0200
@@ -917,16 +917,16 @@
 fun rule_tac ctxt [] facts = some_rule_tac ctxt facts
   | rule_tac ctxt rules facts = Method.rule_tac ctxt rules facts;
 
-fun standard_tac ctxt rules facts =
-  HEADGOAL (rule_tac ctxt rules facts) ORELSE
+fun standard_tac ctxt facts =
+  HEADGOAL (some_rule_tac ctxt facts) ORELSE
   Class.standard_intro_classes_tac ctxt facts;
 
-fun default_tac rules ctxt facts st =
+fun default_tac ctxt facts st =
   (if Method.detect_closure_state st then
     legacy_feature
       ("Old method \"default\"; use \"standard\" instead" ^ Position.here (Position.thread_data ()))
    else ();
-   standard_tac rules ctxt facts st);
+   standard_tac ctxt facts st);
 
 end;
 
@@ -951,11 +951,9 @@
 
 val _ =
   Theory.setup
-   (Method.setup @{binding standard}
-     (Attrib.thms >> (fn rules => fn ctxt => METHOD (standard_tac ctxt rules)))
+   (Method.setup @{binding standard} (Scan.succeed (METHOD o standard_tac))
       "standard proof step: classical intro/elim rule or class introduction" #>
-    Method.setup @{binding default}
-     (Attrib.thms >> (fn rules => fn ctxt => METHOD (default_tac ctxt rules)))
+    Method.setup @{binding default} (Scan.succeed (METHOD o default_tac))
       "standard proof step: classical intro/elim rule or class introduction (legacy)" #>
     Method.setup @{binding rule}
       (Attrib.thms >> (fn rules => fn ctxt => METHOD (HEADGOAL o rule_tac ctxt rules)))
diff -r 4c79543cc376 -r 7512716f03db src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Tue Jun 30 15:20:56 2015 +0200
+++ b/src/Pure/Isar/class.ML	Tue Jun 30 15:41:11 2015 +0200
@@ -762,23 +762,23 @@
     (intro_classes_tac ctxt [] ORELSE Locale.intro_locales_tac true ctxt []) st
   else no_tac st;
 
-fun standard_tac rules ctxt facts =
-  HEADGOAL (Method.some_rule_tac ctxt rules facts) ORELSE
+fun standard_tac ctxt facts =
+  HEADGOAL (Method.some_rule_tac ctxt [] facts) ORELSE
   standard_intro_classes_tac ctxt facts;
 
-fun default_tac rules ctxt facts st =
+fun default_tac ctxt facts st =
   (if Method.detect_closure_state st then
     legacy_feature
       ("Old method \"default\"; use \"standard\" instead" ^ Position.here (Position.thread_data ()))
    else ();
-   standard_tac rules ctxt facts st);
+   standard_tac ctxt facts st);
 
 val _ = Theory.setup
  (Method.setup @{binding intro_classes} (Scan.succeed (METHOD o intro_classes_tac))
     "back-chain introduction rules of classes" #>
-  Method.setup @{binding standard} (Attrib.thms >> (METHOD oo standard_tac))
+  Method.setup @{binding standard} (Scan.succeed (METHOD o standard_tac))
     "standard proof step: Pure intro/elim rule or class introduction" #>
-  Method.setup @{binding default} (Attrib.thms >> (METHOD oo default_tac))
+  Method.setup @{binding default} (Scan.succeed (METHOD o default_tac))
     "standard proof step: Pure intro/elim rule or class introduction (legacy)");