# HG changeset patch
# User wenzelm
# Date 1282738689 -7200
# Node ID 8915e3ce8655f45135e9b70a226961a30e6215e0
# Parent  d81f4d84ce3b98d293c7d85c953dff85d580c705
discontinued obsolete 'global' and 'local' commands;

diff -r d81f4d84ce3b -r 8915e3ce8655 NEWS
--- a/NEWS	Wed Aug 25 11:30:45 2010 +0200
+++ b/NEWS	Wed Aug 25 14:18:09 2010 +0200
@@ -32,6 +32,11 @@
 * Diagnostic command 'print_interps' prints interpretations in proofs
 in addition to interpretations in theories.
 
+* Discontinued obsolete 'global' and 'local' commands to manipulate
+the theory name space.  Rare INCOMPATIBILITY.  The ML functions
+Sign.root_path and Sign.local_path may be applied directly where this
+feature is still required for historical reasons.
+
 
 *** HOL ***
 
diff -r d81f4d84ce3b -r 8915e3ce8655 doc-src/IsarRef/Thy/Spec.thy
--- a/doc-src/IsarRef/Thy/Spec.thy	Wed Aug 25 11:30:45 2010 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy	Wed Aug 25 14:18:09 2010 +0200
@@ -1220,8 +1220,6 @@
 
 text {*
   \begin{matharray}{rcl}
-    @{command_def "global"} & : & @{text "theory \<rightarrow> theory"} \\
-    @{command_def "local"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def "hide_class"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def "hide_type"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def "hide_const"} & : & @{text "theory \<rightarrow> theory"} \\
@@ -1241,16 +1239,6 @@
 
   \begin{description}
 
-  \item @{command "global"} and @{command "local"} change the current
-  name declaration mode.  Initially, theories start in @{command
-  "local"} mode, causing all names to be automatically qualified by
-  the theory name.  Changing this to @{command "global"} causes all
-  names to be declared without the theory prefix, until @{command
-  "local"} is declared again.
-  
-  Note that global names are prone to get hidden accidently later,
-  when qualified names of the same base name are introduced.
-  
   \item @{command "hide_class"}~@{text names} fully removes class
   declarations from a given name space; with the @{text "(open)"}
   option, only the base name is hidden.  Global (unqualified) names
diff -r d81f4d84ce3b -r 8915e3ce8655 doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Wed Aug 25 11:30:45 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Wed Aug 25 14:18:09 2010 +0200
@@ -1262,8 +1262,6 @@
 %
 \begin{isamarkuptext}%
 \begin{matharray}{rcl}
-    \indexdef{}{command}{global}\hypertarget{command.global}{\hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
-    \indexdef{}{command}{local}\hypertarget{command.local}{\hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     \indexdef{}{command}{hide\_class}\hypertarget{command.hide-class}{\hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isacharunderscore}class}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     \indexdef{}{command}{hide\_type}\hypertarget{command.hide-type}{\hyperlink{command.hide-type}{\mbox{\isa{\isacommand{hide{\isacharunderscore}type}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     \indexdef{}{command}{hide\_const}\hypertarget{command.hide-const}{\hyperlink{command.hide-const}{\mbox{\isa{\isacommand{hide{\isacharunderscore}const}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
@@ -1283,14 +1281,6 @@
 
   \begin{description}
 
-  \item \hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} and \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} change the current
-  name declaration mode.  Initially, theories start in \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} mode, causing all names to be automatically qualified by
-  the theory name.  Changing this to \hyperlink{command.global}{\mbox{\isa{\isacommand{global}}}} causes all
-  names to be declared without the theory prefix, until \hyperlink{command.local}{\mbox{\isa{\isacommand{local}}}} is declared again.
-  
-  Note that global names are prone to get hidden accidently later,
-  when qualified names of the same base name are introduced.
-  
   \item \hyperlink{command.hide-class}{\mbox{\isa{\isacommand{hide{\isacharunderscore}class}}}}~\isa{names} fully removes class
   declarations from a given name space; with the \isa{{\isachardoublequote}{\isacharparenleft}open{\isacharparenright}{\isachardoublequote}}
   option, only the base name is hidden.  Global (unqualified) names
diff -r d81f4d84ce3b -r 8915e3ce8655 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Wed Aug 25 11:30:45 2010 +0200
+++ b/etc/isar-keywords-ZF.el	Wed Aug 25 14:18:09 2010 +0200
@@ -73,7 +73,6 @@
     "fix"
     "from"
     "full_prf"
-    "global"
     "guess"
     "have"
     "header"
@@ -97,7 +96,6 @@
     "lemmas"
     "let"
     "linear_undo"
-    "local"
     "local_setup"
     "locale"
     "method_setup"
@@ -369,7 +367,6 @@
     "extract"
     "extract_type"
     "finalconsts"
-    "global"
     "hide_class"
     "hide_const"
     "hide_fact"
@@ -378,7 +375,6 @@
     "instantiation"
     "judgment"
     "lemmas"
-    "local"
     "local_setup"
     "locale"
     "method_setup"
diff -r d81f4d84ce3b -r 8915e3ce8655 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Wed Aug 25 11:30:45 2010 +0200
+++ b/etc/isar-keywords.el	Wed Aug 25 14:18:09 2010 +0200
@@ -102,7 +102,6 @@
     "full_prf"
     "fun"
     "function"
-    "global"
     "guess"
     "have"
     "header"
@@ -128,7 +127,6 @@
     "lemmas"
     "let"
     "linear_undo"
-    "local"
     "local_setup"
     "locale"
     "method_setup"
@@ -469,7 +467,6 @@
     "fixpat"
     "fixrec"
     "fun"
-    "global"
     "hide_class"
     "hide_const"
     "hide_fact"
@@ -479,7 +476,6 @@
     "instantiation"
     "judgment"
     "lemmas"
-    "local"
     "local_setup"
     "locale"
     "method_setup"
diff -r d81f4d84ce3b -r 8915e3ce8655 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Aug 25 11:30:45 2010 +0200
+++ b/src/HOL/HOL.thy	Wed Aug 25 14:18:09 2010 +0200
@@ -57,14 +57,18 @@
   False         :: bool
   Not           :: "bool => bool"                   ("~ _" [40] 40)
 
-global consts
+setup Sign.root_path
+
+consts
   "op &"        :: "[bool, bool] => bool"           (infixr "&" 35)
   "op |"        :: "[bool, bool] => bool"           (infixr "|" 30)
   "op -->"      :: "[bool, bool] => bool"           (infixr "-->" 25)
 
   "op ="        :: "['a, 'a] => bool"               (infixl "=" 50)
 
-local consts
+setup Sign.local_path
+
+consts
   The           :: "('a => bool) => 'a"
   All           :: "('a => bool) => bool"           (binder "ALL " 10)
   Ex            :: "('a => bool) => bool"           (binder "EX " 10)
diff -r d81f4d84ce3b -r 8915e3ce8655 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Aug 25 11:30:45 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Aug 25 14:18:09 2010 +0200
@@ -286,14 +286,6 @@
 
 (* name space entry path *)
 
-val _ =
-  Outer_Syntax.command "global" "disable prefixing of theory name" Keyword.thy_decl
-    (Scan.succeed (Toplevel.theory Sign.root_path));
-
-val _ =
-  Outer_Syntax.command "local" "enable prefixing of theory name" Keyword.thy_decl
-    (Scan.succeed (Toplevel.theory Sign.local_path));
-
 fun hide_names name hide what =
   Outer_Syntax.command name ("hide " ^ what ^ " from name space") Keyword.thy_decl
     ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 Parse.xname >>