# HG changeset patch
# User wenzelm
# Date 1390741279 -3600
# Node ID a56099a6447af7d1c651cd0899ffa0d1be05014d
# Parent  f331472f102753d83de11d42366745850588fd35
discontinued obsolete attribute "standard";

diff -r f331472f1027 -r a56099a6447a NEWS
--- a/NEWS	Sun Jan 26 13:45:40 2014 +0100
+++ b/NEWS	Sun Jan 26 14:01:19 2014 +0100
@@ -44,6 +44,15 @@
 variables ('for' declaration): these variables become schematic in the
 instantiated theorem.
 
+* Obsolete attribute "standard" has been discontinued (legacy since
+Isabelle2012).  Potential INCOMPATIBILITY, use explicit 'for' context
+where instantiations with schematic variables are intended (for
+declaration commands like 'lemmas' or attributes like "of").  The
+following temporary definition may help to port old applications:
+
+  attribute_setup standard =
+    "Scan.succeed (Thm.rule_attribute (K Drule.export_without_context))"
+
 * More thorough check of proof context for goal statements and
 attributed fact expressions (concerning background theory, declared
 hyps).  Potential INCOMPATIBILITY, tools need to observe standard
diff -r f331472f1027 -r a56099a6447a src/Doc/IsarRef/Generic.thy
--- a/src/Doc/IsarRef/Generic.thy	Sun Jan 26 13:45:40 2014 +0100
+++ b/src/Doc/IsarRef/Generic.thy	Sun Jan 26 14:01:19 2014 +0100
@@ -132,7 +132,6 @@
     @{attribute_def abs_def} & : & @{text attribute} \\[0.5ex]
     @{attribute_def rotated} & : & @{text attribute} \\
     @{attribute_def (Pure) elim_format} & : & @{text attribute} \\
-    @{attribute_def standard}@{text "\<^sup>*"} & : & @{text attribute} \\
     @{attribute_def no_vars}@{text "\<^sup>*"} & : & @{text attribute} \\
   \end{matharray}
 
@@ -180,11 +179,6 @@
   Note that the Classical Reasoner (\secref{sec:classical}) provides
   its own version of this operation.
 
-  \item @{attribute standard} puts a theorem into the standard form of
-  object-rules at the outermost theory level.  Note that this
-  operation violates the local proof context (including active
-  locales).
-
   \item @{attribute no_vars} replaces schematic variables by free
   ones; this is mainly for tuning output of pretty printed theorems.
 
diff -r f331472f1027 -r a56099a6447a src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sun Jan 26 13:45:40 2014 +0100
+++ b/src/Pure/Pure.thy	Sun Jan 26 14:01:19 2014 +0100
@@ -175,10 +175,6 @@
   "Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params"
   "named rule parameters"
 
-attribute_setup standard =
-  "Scan.succeed (Thm.rule_attribute (K Drule.export_without_context))"
-  "result put into standard form (legacy)"
-
 attribute_setup rule_format = {*
   Scan.lift (Args.mode "no_asm")
     >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format)