# HG changeset patch
# User wenzelm
# Date 1428087896 -7200
# Node ID 5b919b13feeea78c9eaada3a35ba21432914c5db
# Parent  86d302846b16d3a8520ed33eb2b8ea4ca450720b
obsolete (see 8b7caf447357);

diff -r 86d302846b16 -r 5b919b13feee src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Fri Apr 03 20:52:17 2015 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy	Fri Apr 03 21:04:56 2015 +0200
@@ -27,11 +27,7 @@
 end
 (*<*)end(*>*)
 
-text \<open>For historical reasons, some tools cannot take the full proof
-  context into account and merely refer to the background theory.
-  This is accommodated by configuration options being declared as
-  ``global'', which may not be changed within a local context.
-
+text \<open>
   \begin{matharray}{rcll}
     @{command_def "print_options"} & : & @{text "context \<rightarrow>"} \\
   \end{matharray}