--- 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 ***
--- 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
--- 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
--- 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"
--- 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"
--- 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)
--- 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 >>