src/Pure/Isar/class.ML

--- a/src/Pure/Isar/class.ML	Sat Apr 09 20:38:08 2016 +0200
+++ b/src/Pure/Isar/class.ML	Sat Apr 09 21:42:42 2016 +0200
@@ -768,20 +768,11 @@
   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");