# HG changeset patch
# User wenzelm
# Date 1428604958 -7200
# Node ID 09be0495dcc2015aea497ca978d59bbd1e672822
# Parent  7b80ddb65e3e18b3992404c704369d1ced98e97e# Parent  a81dc82ecba3f7dc1abb30a40aa20bdf1f8d6c70
merged

diff -r 7b80ddb65e3e -r 09be0495dcc2 NEWS
--- a/NEWS	Thu Apr 09 18:46:16 2015 +0200
+++ b/NEWS	Thu Apr 09 20:42:38 2015 +0200
@@ -7,17 +7,18 @@
 *** General ***
 
 * Local theory specification commands may have a 'private' or
-'restricted' modifier to limit name space accesses to the local scope,
+'qualified' modifier to restrict name space accesses to the local scope,
 as provided by some "context begin ... end" block. For example:
 
   context
   begin
 
   private definition ...
-  private definition ...
   private lemma ...
 
-  lemma ...
+  qualified definition ...
+  qualified lemma ...
+
   lemma ...
   theorem ...
 
diff -r 7b80ddb65e3e -r 09be0495dcc2 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Thu Apr 09 18:46:16 2015 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Thu Apr 09 20:42:38 2015 +0200
@@ -115,7 +115,7 @@
     @{command_def "context"} & : & @{text "theory \<rightarrow> local_theory"} \\
     @{command_def (local) "end"} & : & @{text "local_theory \<rightarrow> theory"} \\
     @{keyword_def "private"} \\
-    @{keyword_def "restricted"} \\
+    @{keyword_def "qualified"} \\
   \end{matharray}
 
   A local theory target is a specification context that is managed
@@ -162,16 +162,16 @@
   (global) "end"} has a different meaning: it concludes the theory
   itself (\secref{sec:begin-thy}).
   
-  \item @{keyword "private"} or @{keyword "restricted"} may be given as
-  modifiers before any local theory command. This limits name space accesses
-  to the local scope, as determined by the enclosing @{command
+  \item @{keyword "private"} or @{keyword "qualified"} may be given as
+  modifiers before any local theory command. This restricts name space
+  accesses to the local scope, as determined by the enclosing @{command
   "context"}~@{keyword "begin"}~\dots~@{command "end"} block. Outside its
   scope, a @{keyword "private"} name is inaccessible, and a @{keyword
-  "restricted"} name is only accessible with additional qualification.
+  "qualified"} name is only accessible with additional qualification.
 
   Neither a global @{command theory} nor a @{command locale} target provides
   a local scope by itself: an extra unnamed context is required to use
-  @{keyword "private"} or @{keyword "restricted"} here.
+  @{keyword "private"} or @{keyword "qualified"} here.
 
   \item @{text "("}@{keyword_def "in"}~@{text "c)"} given after any local
   theory command specifies an immediate target, e.g.\ ``@{command
diff -r 7b80ddb65e3e -r 09be0495dcc2 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Thu Apr 09 18:46:16 2015 +0200
+++ b/src/FOL/FOL.thy	Thu Apr 09 20:42:38 2015 +0200
@@ -387,10 +387,10 @@
 context
 begin
 
-restricted definition "induct_forall(P) \<equiv> \<forall>x. P(x)"
-restricted definition "induct_implies(A, B) \<equiv> A \<longrightarrow> B"
-restricted definition "induct_equal(x, y) \<equiv> x = y"
-restricted definition "induct_conj(A, B) \<equiv> A \<and> B"
+qualified definition "induct_forall(P) \<equiv> \<forall>x. P(x)"
+qualified definition "induct_implies(A, B) \<equiv> A \<longrightarrow> B"
+qualified definition "induct_equal(x, y) \<equiv> x = y"
+qualified definition "induct_conj(A, B) \<equiv> A \<and> B"
 
 lemma induct_forall_eq: "(\<And>x. P(x)) \<equiv> Trueprop(induct_forall(\<lambda>x. P(x)))"
   unfolding atomize_all induct_forall_def .
diff -r 7b80ddb65e3e -r 09be0495dcc2 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Apr 09 18:46:16 2015 +0200
+++ b/src/HOL/HOL.thy	Thu Apr 09 20:42:38 2015 +0200
@@ -1377,12 +1377,12 @@
 context
 begin
 
-restricted definition "induct_forall P \<equiv> \<forall>x. P x"
-restricted definition "induct_implies A B \<equiv> A \<longrightarrow> B"
-restricted definition "induct_equal x y \<equiv> x = y"
-restricted definition "induct_conj A B \<equiv> A \<and> B"
-restricted definition "induct_true \<equiv> True"
-restricted definition "induct_false \<equiv> False"
+qualified definition "induct_forall P \<equiv> \<forall>x. P x"
+qualified definition "induct_implies A B \<equiv> A \<longrightarrow> B"
+qualified definition "induct_equal x y \<equiv> x = y"
+qualified definition "induct_conj A B \<equiv> A \<and> B"
+qualified definition "induct_true \<equiv> True"
+qualified definition "induct_false \<equiv> False"
 
 lemma induct_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (induct_forall (\<lambda>x. P x))"
   by (unfold atomize_all induct_forall_def)
diff -r 7b80ddb65e3e -r 09be0495dcc2 src/HOL/Library/AList.thy
--- a/src/HOL/Library/AList.thy	Thu Apr 09 18:46:16 2015 +0200
+++ b/src/HOL/Library/AList.thy	Thu Apr 09 20:42:38 2015 +0200
@@ -20,7 +20,7 @@
 
 subsection {* @{text update} and @{text updates} *}
 
-restricted primrec update :: "'key \<Rightarrow> 'val \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+qualified primrec update :: "'key \<Rightarrow> 'val \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
   "update k v [] = [(k, v)]"
 | "update k v (p # ps) = (if fst p = k then (k, v) # ps else p # update k v ps)"
@@ -86,7 +86,7 @@
   "x \<notin> A \<Longrightarrow> map_of (update x y al) ` A = map_of al ` A"
   by (simp add: update_conv')
 
-restricted definition
+qualified definition
     updates :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   where "updates ks vs = fold (case_prod update) (zip ks vs)"
 
@@ -165,7 +165,7 @@
 
 subsection {* @{text delete} *}
 
-restricted definition delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+qualified definition delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   where delete_eq: "delete k = filter (\<lambda>(k', _). k \<noteq> k')"
 
 lemma delete_simps [simp]:
@@ -217,7 +217,7 @@
 
 subsection {* @{text restrict} *}
 
-restricted definition restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+qualified definition restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   where restrict_eq: "restrict A = filter (\<lambda>(k, v). k \<in> A)"
 
 lemma restr_simps [simp]:
@@ -301,7 +301,7 @@
 
 subsection {* @{text clearjunk} *}
 
-restricted function clearjunk  :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+qualified function clearjunk  :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
   "clearjunk [] = []"
 | "clearjunk (p#ps) = p # clearjunk (delete (fst p) ps)"
@@ -411,7 +411,7 @@
 
 subsection {* @{text merge} *}
 
-restricted definition merge :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+qualified definition merge :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
   where "merge qs ps = foldr (\<lambda>(k, v). update k v) ps qs"
 
 lemma merge_simps [simp]:
@@ -479,7 +479,7 @@
 
 subsection {* @{text compose} *}
 
-restricted function compose :: "('key \<times> 'a) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('key \<times> 'b) list"
+qualified function compose :: "('key \<times> 'a) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('key \<times> 'b) list"
 where
   "compose [] ys = []"
 | "compose (x # xs) ys =
@@ -644,7 +644,7 @@
 
 subsection {* @{text map_entry} *}
 
-restricted fun map_entry :: "'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
+qualified fun map_entry :: "'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
 where
   "map_entry k f [] = []"
 | "map_entry k f (p # ps) =
diff -r 7b80ddb65e3e -r 09be0495dcc2 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Thu Apr 09 18:46:16 2015 +0200
+++ b/src/Pure/General/binding.ML	Thu Apr 09 20:42:38 2015 +0200
@@ -30,9 +30,7 @@
   val prefix_of: binding -> (string * bool) list
   val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
   val prefix: bool -> string -> binding -> binding
-  val private: scope -> binding -> binding
-  val restricted: scope -> binding -> binding
-  val limited_default: (bool * scope) option -> binding -> binding
+  val restricted_default: (bool * scope) option -> binding -> binding
   val concealed: binding -> binding
   val pretty: binding -> Pretty.T
   val print: binding -> string
@@ -40,7 +38,7 @@
   val bad: binding -> string
   val check: binding -> unit
   val name_spec: scope list -> (string * bool) list -> binding ->
-    {limitation: bool option, concealed: bool, spec: (string * bool) list}
+    {restriction: bool option, concealed: bool, spec: (string * bool) list}
 end;
 
 structure Binding: BINDING =
@@ -48,7 +46,7 @@
 
 (** representation **)
 
-(* scope of limited entries *)
+(* scope of restricted entries *)
 
 datatype scope = Scope of serial;
 
@@ -58,19 +56,19 @@
 (* binding *)
 
 datatype binding = Binding of
- {limited: (bool * scope) option,  (*entry is private (true) / restricted (false) to scope*)
-  concealed: bool,                 (*entry is for foundational purposes -- please ignore*)
-  prefix: (string * bool) list,    (*system prefix*)
-  qualifier: (string * bool) list, (*user qualifier*)
-  name: bstring,                   (*base name*)
-  pos: Position.T};                (*source position*)
+ {restricted: (bool * scope) option,  (*entry is private (true) or qualified (false) wrt. scope*)
+  concealed: bool,  (*entry is for foundational purposes -- please ignore*)
+  prefix: (string * bool) list,  (*system prefix*)
+  qualifier: (string * bool) list,  (*user qualifier*)
+  name: bstring,  (*base name*)
+  pos: Position.T};  (*source position*)
 
-fun make_binding (limited, concealed, prefix, qualifier, name, pos) =
-  Binding {limited = limited, concealed = concealed, prefix = prefix,
+fun make_binding (restricted, concealed, prefix, qualifier, name, pos) =
+  Binding {restricted = restricted, concealed = concealed, prefix = prefix,
     qualifier = qualifier, name = name, pos = pos};
 
-fun map_binding f (Binding {limited, concealed, prefix, qualifier, name, pos}) =
-  make_binding (f (limited, concealed, prefix, qualifier, name, pos));
+fun map_binding f (Binding {restricted, concealed, prefix, qualifier, name, pos}) =
+  make_binding (f (restricted, concealed, prefix, qualifier, name, pos));
 
 fun path_of (Binding {prefix, qualifier, ...}) = prefix @ qualifier;
 
@@ -84,8 +82,8 @@
 
 fun pos_of (Binding {pos, ...}) = pos;
 fun set_pos pos =
-  map_binding (fn (limited, concealed, prefix, qualifier, name, _) =>
-    (limited, concealed, prefix, qualifier, name, pos));
+  map_binding (fn (restricted, concealed, prefix, qualifier, name, _) =>
+    (restricted, concealed, prefix, qualifier, name, pos));
 
 fun name name = make (name, Position.none);
 fun name_of (Binding {name, ...}) = name;
@@ -93,8 +91,8 @@
 fun eq_name (b, b') = name_of b = name_of b';
 
 fun map_name f =
-  map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
-    (limited, concealed, prefix, qualifier, f name, pos));
+  map_binding (fn (restricted, concealed, prefix, qualifier, name, pos) =>
+    (restricted, concealed, prefix, qualifier, f name, pos));
 
 val prefix_name = map_name o prefix;
 val suffix_name = map_name o suffix;
@@ -107,13 +105,13 @@
 
 fun qualify _ "" = I
   | qualify mandatory qual =
-      map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
-        (limited, concealed, prefix, (qual, mandatory) :: qualifier, name, pos));
+      map_binding (fn (restricted, concealed, prefix, qualifier, name, pos) =>
+        (restricted, concealed, prefix, (qual, mandatory) :: qualifier, name, pos));
 
 fun qualified mandatory name' =
-  map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
+  map_binding (fn (restricted, concealed, prefix, qualifier, name, pos) =>
     let val qualifier' = if name = "" then qualifier else qualifier @ [(name, mandatory)]
-    in (limited, concealed, prefix, qualifier', name', pos) end);
+    in (restricted, concealed, prefix, qualifier', name', pos) end);
 
 fun qualified_name "" = empty
   | qualified_name s =
@@ -126,8 +124,8 @@
 fun prefix_of (Binding {prefix, ...}) = prefix;
 
 fun map_prefix f =
-  map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
-    (limited, concealed, f prefix, qualifier, name, pos));
+  map_binding (fn (restricted, concealed, prefix, qualifier, name, pos) =>
+    (restricted, concealed, f prefix, qualifier, name, pos));
 
 fun prefix _ "" = I
   | prefix mandatory prfx = map_prefix (cons (prfx, mandatory));
@@ -135,20 +133,18 @@
 
 (* visibility flags *)
 
-fun limited strict scope =
+fun restricted strict scope =
   map_binding (fn (_, concealed, prefix, qualifier, name, pos) =>
     (SOME (strict, scope), concealed, prefix, qualifier, name, pos));
 
-val private = limited true;
-val restricted = limited false;
-
-fun limited_default limited' =
-  map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
-    (if is_some limited then limited else limited', concealed, prefix, qualifier, name, pos));
+fun restricted_default restricted' =
+  map_binding (fn (restricted, concealed, prefix, qualifier, name, pos) =>
+    (if is_some restricted then restricted else restricted',
+      concealed, prefix, qualifier, name, pos));
 
 val concealed =
-  map_binding (fn (limited, _, prefix, qualifier, name, pos) =>
-    (limited, true, prefix, qualifier, name, pos));
+  map_binding (fn (restricted, _, prefix, qualifier, name, pos) =>
+    (restricted, true, prefix, qualifier, name, pos));
 
 
 (* print *)
@@ -181,11 +177,11 @@
 
 fun name_spec scopes path binding =
   let
-    val Binding {limited, concealed, prefix, qualifier, name, ...} = binding;
+    val Binding {restricted, concealed, prefix, qualifier, name, ...} = binding;
     val _ = Long_Name.is_qualified name andalso error (bad binding);
 
-    val limitation =
-      (case limited of
+    val restriction =
+      (case restricted of
         NONE => NONE
       | SOME (strict, scope) => if member (op =) scopes scope then NONE else SOME strict);
 
@@ -196,7 +192,7 @@
     val _ =
       exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
       andalso error (bad binding);
-  in {limitation = limitation, concealed = concealed, spec = if null spec2 then [] else spec} end;
+  in {restriction = restriction, concealed = concealed, spec = if null spec2 then [] else spec} end;
 
 end;
 
diff -r 7b80ddb65e3e -r 09be0495dcc2 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Thu Apr 09 18:46:16 2015 +0200
+++ b/src/Pure/General/name_space.ML	Thu Apr 09 20:42:38 2015 +0200
@@ -35,11 +35,11 @@
   val get_scopes: naming -> Binding.scope list
   val get_scope: naming -> Binding.scope option
   val new_scope: naming -> Binding.scope * naming
-  val limited: bool -> Position.T -> naming -> naming
+  val restricted: bool -> Position.T -> naming -> naming
   val private_scope: Binding.scope -> naming -> naming
   val private: Position.T -> naming -> naming
-  val restricted_scope: Binding.scope -> naming -> naming
-  val restricted: Position.T -> naming -> naming
+  val qualified_scope: Binding.scope -> naming -> naming
+  val qualified: Position.T -> naming -> naming
   val concealed: naming -> naming
   val get_group: naming -> serial option
   val set_group: serial option -> naming -> naming
@@ -300,21 +300,21 @@
 
 datatype naming = Naming of
  {scopes: Binding.scope list,
-  limited: (bool * Binding.scope) option,
+  restricted: (bool * Binding.scope) option,
   concealed: bool,
   group: serial option,
   theory_name: string,
   path: (string * bool) list};
 
-fun make_naming (scopes, limited, concealed, group, theory_name, path) =
-  Naming {scopes = scopes, limited = limited, concealed = concealed,
+fun make_naming (scopes, restricted, concealed, group, theory_name, path) =
+  Naming {scopes = scopes, restricted = restricted, concealed = concealed,
     group = group, theory_name = theory_name, path = path};
 
-fun map_naming f (Naming {scopes, limited, concealed, group, theory_name, path}) =
-  make_naming (f (scopes, limited, concealed, group, theory_name, path));
+fun map_naming f (Naming {scopes, restricted, concealed, group, theory_name, path}) =
+  make_naming (f (scopes, restricted, concealed, group, theory_name, path));
 
 
-(* scope and access limitation *)
+(* scope and access restriction *)
 
 fun get_scopes (Naming {scopes, ...}) = scopes;
 val get_scope = try hd o get_scopes;
@@ -323,38 +323,38 @@
   let
     val scope = Binding.new_scope ();
     val naming' =
-      naming |> map_naming (fn (scopes, limited, concealed, group, theory_name, path) =>
-        (scope :: scopes, limited, concealed, group, theory_name, path));
+      naming |> map_naming (fn (scopes, restricted, concealed, group, theory_name, path) =>
+        (scope :: scopes, restricted, concealed, group, theory_name, path));
   in (scope, naming') end;
 
-fun limited_scope strict scope =
+fun restricted_scope strict scope =
   map_naming (fn (scopes, _, concealed, group, theory_name, path) =>
     (scopes, SOME (strict, scope), concealed, group, theory_name, path));
 
-fun limited strict pos naming =
+fun restricted strict pos naming =
   (case get_scope naming of
-    SOME scope => limited_scope strict scope naming
-  | NONE => error ("Missing local scope -- cannot limit name space accesses" ^ Position.here pos));
+    SOME scope => restricted_scope strict scope naming
+  | NONE => error ("Missing local scope -- cannot restrict name space accesses" ^ Position.here pos));
 
-val private_scope = limited_scope true;
-val private = limited true;
+val private_scope = restricted_scope true;
+val private = restricted true;
 
-val restricted_scope = limited_scope false;
-val restricted = limited false;
+val qualified_scope = restricted_scope false;
+val qualified = restricted false;
 
-val concealed = map_naming (fn (scopes, limited, _, group, theory_name, path) =>
-  (scopes, limited, true, group, theory_name, path));
+val concealed = map_naming (fn (scopes, restricted, _, group, theory_name, path) =>
+  (scopes, restricted, true, group, theory_name, path));
 
 
 (* additional structural info *)
 
-fun set_theory_name theory_name = map_naming (fn (scopes, limited, concealed, group, _, path) =>
-  (scopes, limited, concealed, group, theory_name, path));
+fun set_theory_name theory_name = map_naming (fn (scopes, restricted, concealed, group, _, path) =>
+  (scopes, restricted, concealed, group, theory_name, path));
 
 fun get_group (Naming {group, ...}) = group;
 
-fun set_group group = map_naming (fn (scopes, limited, concealed, _, theory_name, path) =>
-  (scopes, limited, concealed, group, theory_name, path));
+fun set_group group = map_naming (fn (scopes, restricted, concealed, _, theory_name, path) =>
+  (scopes, restricted, concealed, group, theory_name, path));
 
 fun new_group naming = set_group (SOME (serial ())) naming;
 val reset_group = set_group NONE;
@@ -364,8 +364,8 @@
 
 fun get_path (Naming {path, ...}) = path;
 
-fun map_path f = map_naming (fn (scopes, limited, concealed, group, theory_name, path) =>
-  (scopes, limited, concealed, group, theory_name, f path));
+fun map_path f = map_naming (fn (scopes, restricted, concealed, group, theory_name, path) =>
+  (scopes, restricted, concealed, group, theory_name, f path));
 
 fun add_path elems = map_path (fn path => path @ [(elems, false)]);
 val root_path = map_path (fn _ => []);
@@ -381,14 +381,14 @@
 
 (* transform *)
 
-fun transform_naming (Naming {limited = limited', concealed = concealed', ...}) =
-  (case limited' of
-    SOME (strict, scope) => limited_scope strict scope
+fun transform_naming (Naming {restricted = restricted', concealed = concealed', ...}) =
+  (case restricted' of
+    SOME (strict, scope) => restricted_scope strict scope
   | NONE => I) #>
   concealed' ? concealed;
 
-fun transform_binding (Naming {limited, concealed, ...}) =
-  Binding.limited_default limited #>
+fun transform_binding (Naming {restricted, concealed, ...}) =
+  Binding.restricted_default restricted #>
   concealed ? Binding.concealed;
 
 
@@ -416,10 +416,10 @@
 
 fun accesses naming binding =
   (case name_spec naming binding of
-    {limitation = SOME true, ...} => ([], [])
-  | {limitation, spec, ...} =>
+    {restriction = SOME true, ...} => ([], [])
+  | {restriction, spec, ...} =>
       let
-        val restrict = is_some limitation ? filter (fn [_] => false | _ => true);
+        val restrict = is_some restriction ? filter (fn [_] => false | _ => true);
         val sfxs = restrict (mandatory_suffixes spec);
         val pfxs = restrict (mandatory_prefixes spec);
       in apply2 (map Long_Name.implode) (sfxs @ pfxs, sfxs) end);
diff -r 7b80ddb65e3e -r 09be0495dcc2 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Thu Apr 09 18:46:16 2015 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Apr 09 20:42:38 2015 +0200
@@ -163,7 +163,7 @@
 local
 
 val before_command =
-  Scan.option (Parse.position (Parse.private >> K true || Parse.restricted >> K false));
+  Scan.option (Parse.position (Parse.private >> K true || Parse.qualified >> K false));
 
 fun parse_command thy =
   Scan.ahead (before_command |-- Parse.position Parse.command_) :|-- (fn (name, pos) =>
diff -r 7b80ddb65e3e -r 09be0495dcc2 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Thu Apr 09 18:46:16 2015 +0200
+++ b/src/Pure/Isar/parse.ML	Thu Apr 09 20:42:38 2015 +0200
@@ -104,7 +104,7 @@
   val propp: (string * string list) parser
   val termp: (string * string list) parser
   val private: Position.T parser
-  val restricted: Position.T parser
+  val qualified: Position.T parser
   val target: (xstring * Position.T) parser
   val opt_target: (xstring * Position.T) option parser
   val args: Token.T list parser
@@ -401,7 +401,7 @@
 (* target information *)
 
 val private = position ($$$ "private") >> #2;
-val restricted = position ($$$ "restricted") >> #2;
+val qualified = position ($$$ "qualified") >> #2;
 
 val target = ($$$ "(" -- $$$ "in") |-- !!! (position xname --| $$$ ")");
 val opt_target = Scan.option target;
diff -r 7b80ddb65e3e -r 09be0495dcc2 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Apr 09 18:46:16 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Apr 09 20:42:38 2015 +0200
@@ -38,8 +38,8 @@
   val new_scope: Proof.context -> Binding.scope * Proof.context
   val private_scope: Binding.scope -> Proof.context -> Proof.context
   val private: Position.T -> Proof.context -> Proof.context
-  val restricted_scope: Binding.scope -> Proof.context -> Proof.context
-  val restricted: Position.T -> Proof.context -> Proof.context
+  val qualified_scope: Binding.scope -> Proof.context -> Proof.context
+  val qualified: Position.T -> Proof.context -> Proof.context
   val concealed: Proof.context -> Proof.context
   val class_space: Proof.context -> Name_Space.T
   val type_space: Proof.context -> Name_Space.T
@@ -321,8 +321,8 @@
 
 val private_scope = map_naming o Name_Space.private_scope;
 val private = map_naming o Name_Space.private;
-val restricted_scope = map_naming o Name_Space.restricted_scope;
-val restricted = map_naming o Name_Space.restricted;
+val qualified_scope = map_naming o Name_Space.qualified_scope;
+val qualified = map_naming o Name_Space.qualified;
 
 val concealed = map_naming Name_Space.concealed;
 
diff -r 7b80ddb65e3e -r 09be0495dcc2 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Thu Apr 09 18:46:16 2015 +0200
+++ b/src/Pure/Isar/token.ML	Thu Apr 09 20:42:38 2015 +0200
@@ -247,7 +247,7 @@
 fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
   | keyword_with _ _ = false;
 
-val is_command_modifier = keyword_with (fn x => x = "private" orelse x = "restricted");
+val is_command_modifier = keyword_with (fn x => x = "private" orelse x = "qualified");
 
 fun ident_with pred (Token (_, (Ident, x), _)) = pred x
   | ident_with _ _ = false;
diff -r 7b80ddb65e3e -r 09be0495dcc2 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Thu Apr 09 18:46:16 2015 +0200
+++ b/src/Pure/Isar/token.scala	Thu Apr 09 20:42:38 2015 +0200
@@ -260,7 +260,7 @@
   def is_end: Boolean = is_command && source == "end"
 
   def is_command_modifier: Boolean =
-    is_keyword && (source == "private" || source == "restricted")
+    is_keyword && (source == "private" || source == "qualified")
 
   def is_begin_block: Boolean = is_command && source == "{"
   def is_end_block: Boolean = is_command && source == "}"
diff -r 7b80ddb65e3e -r 09be0495dcc2 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Apr 09 18:46:16 2015 +0200
+++ b/src/Pure/Isar/toplevel.ML	Thu Apr 09 20:42:38 2015 +0200
@@ -412,15 +412,16 @@
         | NONE => raise UNDEF)
     | _ => raise UNDEF));
 
-val limited_context =
-  fn SOME (strict, scope) => Proof_Context.map_naming (Name_Space.limited strict scope) | NONE => I;
+fun restricted_context (SOME (strict, scope)) =
+      Proof_Context.map_naming (Name_Space.restricted strict scope)
+  | restricted_context NONE = I;
 
-fun local_theory' limited target f = present_transaction (fn int =>
+fun local_theory' restricted target f = present_transaction (fn int =>
   (fn Theory (gthy, _) =>
         let
           val (finish, lthy) = Named_Target.switch target gthy;
           val lthy' = lthy
-            |> limited_context limited
+            |> restricted_context restricted
             |> Local_Theory.new_group
             |> f int
             |> Local_Theory.reset_group;
@@ -428,7 +429,7 @@
     | _ => raise UNDEF))
   (K ());
 
-fun local_theory limited target f = local_theory' limited target (K f);
+fun local_theory restricted target f = local_theory' restricted target (K f);
 
 fun present_local_theory target = present_transaction (fn int =>
   (fn Theory (gthy, _) =>
@@ -473,18 +474,18 @@
 
 in
 
-fun local_theory_to_proof' limited target f = begin_proof
+fun local_theory_to_proof' restricted target f = begin_proof
   (fn int => fn gthy =>
     let
       val (finish, lthy) = Named_Target.switch target gthy;
       val prf = lthy
-        |> limited_context limited
+        |> restricted_context restricted
         |> Local_Theory.new_group
         |> f int;
     in (finish o Local_Theory.reset_group, prf) end);
 
-fun local_theory_to_proof limited target f =
-  local_theory_to_proof' limited target (K f);
+fun local_theory_to_proof restricted target f =
+  local_theory_to_proof' restricted target (K f);
 
 fun theory_to_proof f = begin_proof
   (fn _ => fn gthy =>
diff -r 7b80ddb65e3e -r 09be0495dcc2 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Thu Apr 09 18:46:16 2015 +0200
+++ b/src/Pure/Pure.thy	Thu Apr 09 20:42:38 2015 +0200
@@ -11,7 +11,7 @@
     "\<subseteq>" "]" "assumes" "attach" "binder" "constrains"
     "defines" "fixes" "for" "identifier" "if" "in" "includes" "infix"
     "infixl" "infixr" "is" "notes" "obtains" "open" "output"
-    "overloaded" "pervasive" "private" "restricted" "shows"
+    "overloaded" "pervasive" "private" "qualified" "shows"
     "structure" "unchecked" "where" "|"
   and "text" "txt" :: document_body
   and "text_raw" :: document_raw
diff -r 7b80ddb65e3e -r 09be0495dcc2 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Apr 09 18:46:16 2015 +0200
+++ b/src/Pure/sign.ML	Thu Apr 09 20:42:38 2015 +0200
@@ -113,6 +113,8 @@
   val local_path: theory -> theory
   val private_scope: Binding.scope -> theory -> theory
   val private: Position.T -> theory -> theory
+  val qualified_scope: Binding.scope -> theory -> theory
+  val qualified: Position.T -> theory -> theory
   val concealed: theory -> theory
   val hide_class: bool -> string -> theory -> theory
   val hide_type: bool -> string -> theory -> theory
@@ -525,8 +527,8 @@
 
 val private_scope = map_naming o Name_Space.private_scope;
 val private = map_naming o Name_Space.private;
-val restricted_scope = map_naming o Name_Space.restricted_scope;
-val restricted = map_naming o Name_Space.restricted;
+val qualified_scope = map_naming o Name_Space.qualified_scope;
+val qualified = map_naming o Name_Space.qualified;
 val concealed = map_naming Name_Space.concealed;