# HG changeset patch
# User wenzelm
# Date 1460230962 -7200
# Node ID ef8d840f39fbb1222ff4a26c5f31b909ade43fa8
# Parent  79f41fbdf74ab39b75d7212f487b62a7592794cb
removed old proof method "default";

diff -r 79f41fbdf74a -r ef8d840f39fb NEWS
--- a/NEWS	Sat Apr 09 20:38:08 2016 +0200
+++ b/NEWS	Sat Apr 09 21:42:42 2016 +0200
@@ -36,6 +36,9 @@
 * Command '\<proof>' is an alias for 'sorry', with different
 typesetting. E.g. to produce proof holes in examples and documentation.
 
+* The old proof method "default" has been removed (legacy since
+Isabelle2016). INCOMPATIBILITY, use "standard" instead.
+
 
 *** HOL ***
 
diff -r 79f41fbdf74a -r ef8d840f39fb src/Doc/Classes/Classes.thy
--- a/src/Doc/Classes/Classes.thy	Sat Apr 09 20:38:08 2016 +0200
+++ b/src/Doc/Classes/Classes.thy	Sat Apr 09 21:42:42 2016 +0200
@@ -146,7 +146,7 @@
   @{command definition}).  The concluding @{command instance} opens a
   proof that the given parameters actually conform to the class
   specification.  Note that the first proof step is the @{method
-  default} method, which for such instance proofs maps to the @{method
+  standard} method, which for such instance proofs maps to the @{method
   intro_classes} method.  This reduces an instance judgement to the
   relevant primitive proof goals; typically it is the first method
   applied in an instantiation proof.
diff -r 79f41fbdf74a -r ef8d840f39fb src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sat Apr 09 20:38:08 2016 +0200
+++ b/src/Provers/classical.ML	Sat Apr 09 21:42:42 2016 +0200
@@ -941,13 +941,6 @@
   HEADGOAL (some_rule_tac ctxt facts) ORELSE
   Class.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);
-
 end;
 
 
@@ -973,8 +966,6 @@
   Theory.setup
    (Method.setup @{binding standard} (Scan.succeed (METHOD o standard_tac))
       "standard proof step: classical intro/elim rule or class introduction" #>
-    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)))
       "apply some intro/elim rule (potentially classical)" #>
diff -r 79f41fbdf74a -r ef8d840f39fb 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");