src/Pure/Isar/class.ML

 
 fun standard_tac ctxt facts =
   HEADGOAL (Method.some_rule_tac ctxt [] facts) ORELSE
   standard_intro_classes_tac ctxt facts;
 
-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 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} (Scan.succeed (METHOD o standard_tac))
-    "standard proof step: Pure intro/elim rule or class introduction" #>
-  Method.setup @{binding default} (Scan.succeed (METHOD o default_tac))
-    "standard proof step: Pure intro/elim rule or class introduction (legacy)");
+    "standard proof step: Pure intro/elim rule or class introduction");
 
 
 
 (** diagnostics **)