merged
authorwenzelm
Thu Apr 09 20:42:38 2015 +0200 (2015-04-09)
changeset 5999109be0495dcc2
parent 59989 7b80ddb65e3e
parent 59990 a81dc82ecba3
child 59992 d8db5172c23f
child 60017 b785d6d06430
merged
NEWS
     1.1 --- a/NEWS	Thu Apr 09 18:46:16 2015 +0200
     1.2 +++ b/NEWS	Thu Apr 09 20:42:38 2015 +0200
     1.3 @@ -7,17 +7,18 @@
     1.4  *** General ***
     1.5  
     1.6  * Local theory specification commands may have a 'private' or
     1.7 -'restricted' modifier to limit name space accesses to the local scope,
     1.8 +'qualified' modifier to restrict name space accesses to the local scope,
     1.9  as provided by some "context begin ... end" block. For example:
    1.10  
    1.11    context
    1.12    begin
    1.13  
    1.14    private definition ...
    1.15 -  private definition ...
    1.16    private lemma ...
    1.17  
    1.18 -  lemma ...
    1.19 +  qualified definition ...
    1.20 +  qualified lemma ...
    1.21 +
    1.22    lemma ...
    1.23    theorem ...
    1.24  
     2.1 --- a/src/Doc/Isar_Ref/Spec.thy	Thu Apr 09 18:46:16 2015 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Thu Apr 09 20:42:38 2015 +0200
     2.3 @@ -115,7 +115,7 @@
     2.4      @{command_def "context"} & : & @{text "theory \<rightarrow> local_theory"} \\
     2.5      @{command_def (local) "end"} & : & @{text "local_theory \<rightarrow> theory"} \\
     2.6      @{keyword_def "private"} \\
     2.7 -    @{keyword_def "restricted"} \\
     2.8 +    @{keyword_def "qualified"} \\
     2.9    \end{matharray}
    2.10  
    2.11    A local theory target is a specification context that is managed
    2.12 @@ -162,16 +162,16 @@
    2.13    (global) "end"} has a different meaning: it concludes the theory
    2.14    itself (\secref{sec:begin-thy}).
    2.15    
    2.16 -  \item @{keyword "private"} or @{keyword "restricted"} may be given as
    2.17 -  modifiers before any local theory command. This limits name space accesses
    2.18 -  to the local scope, as determined by the enclosing @{command
    2.19 +  \item @{keyword "private"} or @{keyword "qualified"} may be given as
    2.20 +  modifiers before any local theory command. This restricts name space
    2.21 +  accesses to the local scope, as determined by the enclosing @{command
    2.22    "context"}~@{keyword "begin"}~\dots~@{command "end"} block. Outside its
    2.23    scope, a @{keyword "private"} name is inaccessible, and a @{keyword
    2.24 -  "restricted"} name is only accessible with additional qualification.
    2.25 +  "qualified"} name is only accessible with additional qualification.
    2.26  
    2.27    Neither a global @{command theory} nor a @{command locale} target provides
    2.28    a local scope by itself: an extra unnamed context is required to use
    2.29 -  @{keyword "private"} or @{keyword "restricted"} here.
    2.30 +  @{keyword "private"} or @{keyword "qualified"} here.
    2.31  
    2.32    \item @{text "("}@{keyword_def "in"}~@{text "c)"} given after any local
    2.33    theory command specifies an immediate target, e.g.\ ``@{command
     3.1 --- a/src/FOL/FOL.thy	Thu Apr 09 18:46:16 2015 +0200
     3.2 +++ b/src/FOL/FOL.thy	Thu Apr 09 20:42:38 2015 +0200
     3.3 @@ -387,10 +387,10 @@
     3.4  context
     3.5  begin
     3.6  
     3.7 -restricted definition "induct_forall(P) \<equiv> \<forall>x. P(x)"
     3.8 -restricted definition "induct_implies(A, B) \<equiv> A \<longrightarrow> B"
     3.9 -restricted definition "induct_equal(x, y) \<equiv> x = y"
    3.10 -restricted definition "induct_conj(A, B) \<equiv> A \<and> B"
    3.11 +qualified definition "induct_forall(P) \<equiv> \<forall>x. P(x)"
    3.12 +qualified definition "induct_implies(A, B) \<equiv> A \<longrightarrow> B"
    3.13 +qualified definition "induct_equal(x, y) \<equiv> x = y"
    3.14 +qualified definition "induct_conj(A, B) \<equiv> A \<and> B"
    3.15  
    3.16  lemma induct_forall_eq: "(\<And>x. P(x)) \<equiv> Trueprop(induct_forall(\<lambda>x. P(x)))"
    3.17    unfolding atomize_all induct_forall_def .
     4.1 --- a/src/HOL/HOL.thy	Thu Apr 09 18:46:16 2015 +0200
     4.2 +++ b/src/HOL/HOL.thy	Thu Apr 09 20:42:38 2015 +0200
     4.3 @@ -1377,12 +1377,12 @@
     4.4  context
     4.5  begin
     4.6  
     4.7 -restricted definition "induct_forall P \<equiv> \<forall>x. P x"
     4.8 -restricted definition "induct_implies A B \<equiv> A \<longrightarrow> B"
     4.9 -restricted definition "induct_equal x y \<equiv> x = y"
    4.10 -restricted definition "induct_conj A B \<equiv> A \<and> B"
    4.11 -restricted definition "induct_true \<equiv> True"
    4.12 -restricted definition "induct_false \<equiv> False"
    4.13 +qualified definition "induct_forall P \<equiv> \<forall>x. P x"
    4.14 +qualified definition "induct_implies A B \<equiv> A \<longrightarrow> B"
    4.15 +qualified definition "induct_equal x y \<equiv> x = y"
    4.16 +qualified definition "induct_conj A B \<equiv> A \<and> B"
    4.17 +qualified definition "induct_true \<equiv> True"
    4.18 +qualified definition "induct_false \<equiv> False"
    4.19  
    4.20  lemma induct_forall_eq: "(\<And>x. P x) \<equiv> Trueprop (induct_forall (\<lambda>x. P x))"
    4.21    by (unfold atomize_all induct_forall_def)
     5.1 --- a/src/HOL/Library/AList.thy	Thu Apr 09 18:46:16 2015 +0200
     5.2 +++ b/src/HOL/Library/AList.thy	Thu Apr 09 20:42:38 2015 +0200
     5.3 @@ -20,7 +20,7 @@
     5.4  
     5.5  subsection {* @{text update} and @{text updates} *}
     5.6  
     5.7 -restricted primrec update :: "'key \<Rightarrow> 'val \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
     5.8 +qualified primrec update :: "'key \<Rightarrow> 'val \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
     5.9  where
    5.10    "update k v [] = [(k, v)]"
    5.11  | "update k v (p # ps) = (if fst p = k then (k, v) # ps else p # update k v ps)"
    5.12 @@ -86,7 +86,7 @@
    5.13    "x \<notin> A \<Longrightarrow> map_of (update x y al) ` A = map_of al ` A"
    5.14    by (simp add: update_conv')
    5.15  
    5.16 -restricted definition
    5.17 +qualified definition
    5.18      updates :: "'key list \<Rightarrow> 'val list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    5.19    where "updates ks vs = fold (case_prod update) (zip ks vs)"
    5.20  
    5.21 @@ -165,7 +165,7 @@
    5.22  
    5.23  subsection {* @{text delete} *}
    5.24  
    5.25 -restricted definition delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    5.26 +qualified definition delete :: "'key \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    5.27    where delete_eq: "delete k = filter (\<lambda>(k', _). k \<noteq> k')"
    5.28  
    5.29  lemma delete_simps [simp]:
    5.30 @@ -217,7 +217,7 @@
    5.31  
    5.32  subsection {* @{text restrict} *}
    5.33  
    5.34 -restricted definition restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    5.35 +qualified definition restrict :: "'key set \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    5.36    where restrict_eq: "restrict A = filter (\<lambda>(k, v). k \<in> A)"
    5.37  
    5.38  lemma restr_simps [simp]:
    5.39 @@ -301,7 +301,7 @@
    5.40  
    5.41  subsection {* @{text clearjunk} *}
    5.42  
    5.43 -restricted function clearjunk  :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    5.44 +qualified function clearjunk  :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    5.45  where
    5.46    "clearjunk [] = []"
    5.47  | "clearjunk (p#ps) = p # clearjunk (delete (fst p) ps)"
    5.48 @@ -411,7 +411,7 @@
    5.49  
    5.50  subsection {* @{text merge} *}
    5.51  
    5.52 -restricted definition merge :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    5.53 +qualified definition merge :: "('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    5.54    where "merge qs ps = foldr (\<lambda>(k, v). update k v) ps qs"
    5.55  
    5.56  lemma merge_simps [simp]:
    5.57 @@ -479,7 +479,7 @@
    5.58  
    5.59  subsection {* @{text compose} *}
    5.60  
    5.61 -restricted function compose :: "('key \<times> 'a) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('key \<times> 'b) list"
    5.62 +qualified function compose :: "('key \<times> 'a) list \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> ('key \<times> 'b) list"
    5.63  where
    5.64    "compose [] ys = []"
    5.65  | "compose (x # xs) ys =
    5.66 @@ -644,7 +644,7 @@
    5.67  
    5.68  subsection {* @{text map_entry} *}
    5.69  
    5.70 -restricted fun map_entry :: "'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    5.71 +qualified fun map_entry :: "'key \<Rightarrow> ('val \<Rightarrow> 'val) \<Rightarrow> ('key \<times> 'val) list \<Rightarrow> ('key \<times> 'val) list"
    5.72  where
    5.73    "map_entry k f [] = []"
    5.74  | "map_entry k f (p # ps) =
     6.1 --- a/src/Pure/General/binding.ML	Thu Apr 09 18:46:16 2015 +0200
     6.2 +++ b/src/Pure/General/binding.ML	Thu Apr 09 20:42:38 2015 +0200
     6.3 @@ -30,9 +30,7 @@
     6.4    val prefix_of: binding -> (string * bool) list
     6.5    val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
     6.6    val prefix: bool -> string -> binding -> binding
     6.7 -  val private: scope -> binding -> binding
     6.8 -  val restricted: scope -> binding -> binding
     6.9 -  val limited_default: (bool * scope) option -> binding -> binding
    6.10 +  val restricted_default: (bool * scope) option -> binding -> binding
    6.11    val concealed: binding -> binding
    6.12    val pretty: binding -> Pretty.T
    6.13    val print: binding -> string
    6.14 @@ -40,7 +38,7 @@
    6.15    val bad: binding -> string
    6.16    val check: binding -> unit
    6.17    val name_spec: scope list -> (string * bool) list -> binding ->
    6.18 -    {limitation: bool option, concealed: bool, spec: (string * bool) list}
    6.19 +    {restriction: bool option, concealed: bool, spec: (string * bool) list}
    6.20  end;
    6.21  
    6.22  structure Binding: BINDING =
    6.23 @@ -48,7 +46,7 @@
    6.24  
    6.25  (** representation **)
    6.26  
    6.27 -(* scope of limited entries *)
    6.28 +(* scope of restricted entries *)
    6.29  
    6.30  datatype scope = Scope of serial;
    6.31  
    6.32 @@ -58,19 +56,19 @@
    6.33  (* binding *)
    6.34  
    6.35  datatype binding = Binding of
    6.36 - {limited: (bool * scope) option,  (*entry is private (true) / restricted (false) to scope*)
    6.37 -  concealed: bool,                 (*entry is for foundational purposes -- please ignore*)
    6.38 -  prefix: (string * bool) list,    (*system prefix*)
    6.39 -  qualifier: (string * bool) list, (*user qualifier*)
    6.40 -  name: bstring,                   (*base name*)
    6.41 -  pos: Position.T};                (*source position*)
    6.42 + {restricted: (bool * scope) option,  (*entry is private (true) or qualified (false) wrt. scope*)
    6.43 +  concealed: bool,  (*entry is for foundational purposes -- please ignore*)
    6.44 +  prefix: (string * bool) list,  (*system prefix*)
    6.45 +  qualifier: (string * bool) list,  (*user qualifier*)
    6.46 +  name: bstring,  (*base name*)
    6.47 +  pos: Position.T};  (*source position*)
    6.48  
    6.49 -fun make_binding (limited, concealed, prefix, qualifier, name, pos) =
    6.50 -  Binding {limited = limited, concealed = concealed, prefix = prefix,
    6.51 +fun make_binding (restricted, concealed, prefix, qualifier, name, pos) =
    6.52 +  Binding {restricted = restricted, concealed = concealed, prefix = prefix,
    6.53      qualifier = qualifier, name = name, pos = pos};
    6.54  
    6.55 -fun map_binding f (Binding {limited, concealed, prefix, qualifier, name, pos}) =
    6.56 -  make_binding (f (limited, concealed, prefix, qualifier, name, pos));
    6.57 +fun map_binding f (Binding {restricted, concealed, prefix, qualifier, name, pos}) =
    6.58 +  make_binding (f (restricted, concealed, prefix, qualifier, name, pos));
    6.59  
    6.60  fun path_of (Binding {prefix, qualifier, ...}) = prefix @ qualifier;
    6.61  
    6.62 @@ -84,8 +82,8 @@
    6.63  
    6.64  fun pos_of (Binding {pos, ...}) = pos;
    6.65  fun set_pos pos =
    6.66 -  map_binding (fn (limited, concealed, prefix, qualifier, name, _) =>
    6.67 -    (limited, concealed, prefix, qualifier, name, pos));
    6.68 +  map_binding (fn (restricted, concealed, prefix, qualifier, name, _) =>
    6.69 +    (restricted, concealed, prefix, qualifier, name, pos));
    6.70  
    6.71  fun name name = make (name, Position.none);
    6.72  fun name_of (Binding {name, ...}) = name;
    6.73 @@ -93,8 +91,8 @@
    6.74  fun eq_name (b, b') = name_of b = name_of b';
    6.75  
    6.76  fun map_name f =
    6.77 -  map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
    6.78 -    (limited, concealed, prefix, qualifier, f name, pos));
    6.79 +  map_binding (fn (restricted, concealed, prefix, qualifier, name, pos) =>
    6.80 +    (restricted, concealed, prefix, qualifier, f name, pos));
    6.81  
    6.82  val prefix_name = map_name o prefix;
    6.83  val suffix_name = map_name o suffix;
    6.84 @@ -107,13 +105,13 @@
    6.85  
    6.86  fun qualify _ "" = I
    6.87    | qualify mandatory qual =
    6.88 -      map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
    6.89 -        (limited, concealed, prefix, (qual, mandatory) :: qualifier, name, pos));
    6.90 +      map_binding (fn (restricted, concealed, prefix, qualifier, name, pos) =>
    6.91 +        (restricted, concealed, prefix, (qual, mandatory) :: qualifier, name, pos));
    6.92  
    6.93  fun qualified mandatory name' =
    6.94 -  map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
    6.95 +  map_binding (fn (restricted, concealed, prefix, qualifier, name, pos) =>
    6.96      let val qualifier' = if name = "" then qualifier else qualifier @ [(name, mandatory)]
    6.97 -    in (limited, concealed, prefix, qualifier', name', pos) end);
    6.98 +    in (restricted, concealed, prefix, qualifier', name', pos) end);
    6.99  
   6.100  fun qualified_name "" = empty
   6.101    | qualified_name s =
   6.102 @@ -126,8 +124,8 @@
   6.103  fun prefix_of (Binding {prefix, ...}) = prefix;
   6.104  
   6.105  fun map_prefix f =
   6.106 -  map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
   6.107 -    (limited, concealed, f prefix, qualifier, name, pos));
   6.108 +  map_binding (fn (restricted, concealed, prefix, qualifier, name, pos) =>
   6.109 +    (restricted, concealed, f prefix, qualifier, name, pos));
   6.110  
   6.111  fun prefix _ "" = I
   6.112    | prefix mandatory prfx = map_prefix (cons (prfx, mandatory));
   6.113 @@ -135,20 +133,18 @@
   6.114  
   6.115  (* visibility flags *)
   6.116  
   6.117 -fun limited strict scope =
   6.118 +fun restricted strict scope =
   6.119    map_binding (fn (_, concealed, prefix, qualifier, name, pos) =>
   6.120      (SOME (strict, scope), concealed, prefix, qualifier, name, pos));
   6.121  
   6.122 -val private = limited true;
   6.123 -val restricted = limited false;
   6.124 -
   6.125 -fun limited_default limited' =
   6.126 -  map_binding (fn (limited, concealed, prefix, qualifier, name, pos) =>
   6.127 -    (if is_some limited then limited else limited', concealed, prefix, qualifier, name, pos));
   6.128 +fun restricted_default restricted' =
   6.129 +  map_binding (fn (restricted, concealed, prefix, qualifier, name, pos) =>
   6.130 +    (if is_some restricted then restricted else restricted',
   6.131 +      concealed, prefix, qualifier, name, pos));
   6.132  
   6.133  val concealed =
   6.134 -  map_binding (fn (limited, _, prefix, qualifier, name, pos) =>
   6.135 -    (limited, true, prefix, qualifier, name, pos));
   6.136 +  map_binding (fn (restricted, _, prefix, qualifier, name, pos) =>
   6.137 +    (restricted, true, prefix, qualifier, name, pos));
   6.138  
   6.139  
   6.140  (* print *)
   6.141 @@ -181,11 +177,11 @@
   6.142  
   6.143  fun name_spec scopes path binding =
   6.144    let
   6.145 -    val Binding {limited, concealed, prefix, qualifier, name, ...} = binding;
   6.146 +    val Binding {restricted, concealed, prefix, qualifier, name, ...} = binding;
   6.147      val _ = Long_Name.is_qualified name andalso error (bad binding);
   6.148  
   6.149 -    val limitation =
   6.150 -      (case limited of
   6.151 +    val restriction =
   6.152 +      (case restricted of
   6.153          NONE => NONE
   6.154        | SOME (strict, scope) => if member (op =) scopes scope then NONE else SOME strict);
   6.155  
   6.156 @@ -196,7 +192,7 @@
   6.157      val _ =
   6.158        exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
   6.159        andalso error (bad binding);
   6.160 -  in {limitation = limitation, concealed = concealed, spec = if null spec2 then [] else spec} end;
   6.161 +  in {restriction = restriction, concealed = concealed, spec = if null spec2 then [] else spec} end;
   6.162  
   6.163  end;
   6.164  
     7.1 --- a/src/Pure/General/name_space.ML	Thu Apr 09 18:46:16 2015 +0200
     7.2 +++ b/src/Pure/General/name_space.ML	Thu Apr 09 20:42:38 2015 +0200
     7.3 @@ -35,11 +35,11 @@
     7.4    val get_scopes: naming -> Binding.scope list
     7.5    val get_scope: naming -> Binding.scope option
     7.6    val new_scope: naming -> Binding.scope * naming
     7.7 -  val limited: bool -> Position.T -> naming -> naming
     7.8 +  val restricted: bool -> Position.T -> naming -> naming
     7.9    val private_scope: Binding.scope -> naming -> naming
    7.10    val private: Position.T -> naming -> naming
    7.11 -  val restricted_scope: Binding.scope -> naming -> naming
    7.12 -  val restricted: Position.T -> naming -> naming
    7.13 +  val qualified_scope: Binding.scope -> naming -> naming
    7.14 +  val qualified: Position.T -> naming -> naming
    7.15    val concealed: naming -> naming
    7.16    val get_group: naming -> serial option
    7.17    val set_group: serial option -> naming -> naming
    7.18 @@ -300,21 +300,21 @@
    7.19  
    7.20  datatype naming = Naming of
    7.21   {scopes: Binding.scope list,
    7.22 -  limited: (bool * Binding.scope) option,
    7.23 +  restricted: (bool * Binding.scope) option,
    7.24    concealed: bool,
    7.25    group: serial option,
    7.26    theory_name: string,
    7.27    path: (string * bool) list};
    7.28  
    7.29 -fun make_naming (scopes, limited, concealed, group, theory_name, path) =
    7.30 -  Naming {scopes = scopes, limited = limited, concealed = concealed,
    7.31 +fun make_naming (scopes, restricted, concealed, group, theory_name, path) =
    7.32 +  Naming {scopes = scopes, restricted = restricted, concealed = concealed,
    7.33      group = group, theory_name = theory_name, path = path};
    7.34  
    7.35 -fun map_naming f (Naming {scopes, limited, concealed, group, theory_name, path}) =
    7.36 -  make_naming (f (scopes, limited, concealed, group, theory_name, path));
    7.37 +fun map_naming f (Naming {scopes, restricted, concealed, group, theory_name, path}) =
    7.38 +  make_naming (f (scopes, restricted, concealed, group, theory_name, path));
    7.39  
    7.40  
    7.41 -(* scope and access limitation *)
    7.42 +(* scope and access restriction *)
    7.43  
    7.44  fun get_scopes (Naming {scopes, ...}) = scopes;
    7.45  val get_scope = try hd o get_scopes;
    7.46 @@ -323,38 +323,38 @@
    7.47    let
    7.48      val scope = Binding.new_scope ();
    7.49      val naming' =
    7.50 -      naming |> map_naming (fn (scopes, limited, concealed, group, theory_name, path) =>
    7.51 -        (scope :: scopes, limited, concealed, group, theory_name, path));
    7.52 +      naming |> map_naming (fn (scopes, restricted, concealed, group, theory_name, path) =>
    7.53 +        (scope :: scopes, restricted, concealed, group, theory_name, path));
    7.54    in (scope, naming') end;
    7.55  
    7.56 -fun limited_scope strict scope =
    7.57 +fun restricted_scope strict scope =
    7.58    map_naming (fn (scopes, _, concealed, group, theory_name, path) =>
    7.59      (scopes, SOME (strict, scope), concealed, group, theory_name, path));
    7.60  
    7.61 -fun limited strict pos naming =
    7.62 +fun restricted strict pos naming =
    7.63    (case get_scope naming of
    7.64 -    SOME scope => limited_scope strict scope naming
    7.65 -  | NONE => error ("Missing local scope -- cannot limit name space accesses" ^ Position.here pos));
    7.66 +    SOME scope => restricted_scope strict scope naming
    7.67 +  | NONE => error ("Missing local scope -- cannot restrict name space accesses" ^ Position.here pos));
    7.68  
    7.69 -val private_scope = limited_scope true;
    7.70 -val private = limited true;
    7.71 +val private_scope = restricted_scope true;
    7.72 +val private = restricted true;
    7.73  
    7.74 -val restricted_scope = limited_scope false;
    7.75 -val restricted = limited false;
    7.76 +val qualified_scope = restricted_scope false;
    7.77 +val qualified = restricted false;
    7.78  
    7.79 -val concealed = map_naming (fn (scopes, limited, _, group, theory_name, path) =>
    7.80 -  (scopes, limited, true, group, theory_name, path));
    7.81 +val concealed = map_naming (fn (scopes, restricted, _, group, theory_name, path) =>
    7.82 +  (scopes, restricted, true, group, theory_name, path));
    7.83  
    7.84  
    7.85  (* additional structural info *)
    7.86  
    7.87 -fun set_theory_name theory_name = map_naming (fn (scopes, limited, concealed, group, _, path) =>
    7.88 -  (scopes, limited, concealed, group, theory_name, path));
    7.89 +fun set_theory_name theory_name = map_naming (fn (scopes, restricted, concealed, group, _, path) =>
    7.90 +  (scopes, restricted, concealed, group, theory_name, path));
    7.91  
    7.92  fun get_group (Naming {group, ...}) = group;
    7.93  
    7.94 -fun set_group group = map_naming (fn (scopes, limited, concealed, _, theory_name, path) =>
    7.95 -  (scopes, limited, concealed, group, theory_name, path));
    7.96 +fun set_group group = map_naming (fn (scopes, restricted, concealed, _, theory_name, path) =>
    7.97 +  (scopes, restricted, concealed, group, theory_name, path));
    7.98  
    7.99  fun new_group naming = set_group (SOME (serial ())) naming;
   7.100  val reset_group = set_group NONE;
   7.101 @@ -364,8 +364,8 @@
   7.102  
   7.103  fun get_path (Naming {path, ...}) = path;
   7.104  
   7.105 -fun map_path f = map_naming (fn (scopes, limited, concealed, group, theory_name, path) =>
   7.106 -  (scopes, limited, concealed, group, theory_name, f path));
   7.107 +fun map_path f = map_naming (fn (scopes, restricted, concealed, group, theory_name, path) =>
   7.108 +  (scopes, restricted, concealed, group, theory_name, f path));
   7.109  
   7.110  fun add_path elems = map_path (fn path => path @ [(elems, false)]);
   7.111  val root_path = map_path (fn _ => []);
   7.112 @@ -381,14 +381,14 @@
   7.113  
   7.114  (* transform *)
   7.115  
   7.116 -fun transform_naming (Naming {limited = limited', concealed = concealed', ...}) =
   7.117 -  (case limited' of
   7.118 -    SOME (strict, scope) => limited_scope strict scope
   7.119 +fun transform_naming (Naming {restricted = restricted', concealed = concealed', ...}) =
   7.120 +  (case restricted' of
   7.121 +    SOME (strict, scope) => restricted_scope strict scope
   7.122    | NONE => I) #>
   7.123    concealed' ? concealed;
   7.124  
   7.125 -fun transform_binding (Naming {limited, concealed, ...}) =
   7.126 -  Binding.limited_default limited #>
   7.127 +fun transform_binding (Naming {restricted, concealed, ...}) =
   7.128 +  Binding.restricted_default restricted #>
   7.129    concealed ? Binding.concealed;
   7.130  
   7.131  
   7.132 @@ -416,10 +416,10 @@
   7.133  
   7.134  fun accesses naming binding =
   7.135    (case name_spec naming binding of
   7.136 -    {limitation = SOME true, ...} => ([], [])
   7.137 -  | {limitation, spec, ...} =>
   7.138 +    {restriction = SOME true, ...} => ([], [])
   7.139 +  | {restriction, spec, ...} =>
   7.140        let
   7.141 -        val restrict = is_some limitation ? filter (fn [_] => false | _ => true);
   7.142 +        val restrict = is_some restriction ? filter (fn [_] => false | _ => true);
   7.143          val sfxs = restrict (mandatory_suffixes spec);
   7.144          val pfxs = restrict (mandatory_prefixes spec);
   7.145        in apply2 (map Long_Name.implode) (sfxs @ pfxs, sfxs) end);
     8.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Apr 09 18:46:16 2015 +0200
     8.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Apr 09 20:42:38 2015 +0200
     8.3 @@ -163,7 +163,7 @@
     8.4  local
     8.5  
     8.6  val before_command =
     8.7 -  Scan.option (Parse.position (Parse.private >> K true || Parse.restricted >> K false));
     8.8 +  Scan.option (Parse.position (Parse.private >> K true || Parse.qualified >> K false));
     8.9  
    8.10  fun parse_command thy =
    8.11    Scan.ahead (before_command |-- Parse.position Parse.command_) :|-- (fn (name, pos) =>
     9.1 --- a/src/Pure/Isar/parse.ML	Thu Apr 09 18:46:16 2015 +0200
     9.2 +++ b/src/Pure/Isar/parse.ML	Thu Apr 09 20:42:38 2015 +0200
     9.3 @@ -104,7 +104,7 @@
     9.4    val propp: (string * string list) parser
     9.5    val termp: (string * string list) parser
     9.6    val private: Position.T parser
     9.7 -  val restricted: Position.T parser
     9.8 +  val qualified: Position.T parser
     9.9    val target: (xstring * Position.T) parser
    9.10    val opt_target: (xstring * Position.T) option parser
    9.11    val args: Token.T list parser
    9.12 @@ -401,7 +401,7 @@
    9.13  (* target information *)
    9.14  
    9.15  val private = position ($$$ "private") >> #2;
    9.16 -val restricted = position ($$$ "restricted") >> #2;
    9.17 +val qualified = position ($$$ "qualified") >> #2;
    9.18  
    9.19  val target = ($$$ "(" -- $$$ "in") |-- !!! (position xname --| $$$ ")");
    9.20  val opt_target = Scan.option target;
    10.1 --- a/src/Pure/Isar/proof_context.ML	Thu Apr 09 18:46:16 2015 +0200
    10.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Apr 09 20:42:38 2015 +0200
    10.3 @@ -38,8 +38,8 @@
    10.4    val new_scope: Proof.context -> Binding.scope * Proof.context
    10.5    val private_scope: Binding.scope -> Proof.context -> Proof.context
    10.6    val private: Position.T -> Proof.context -> Proof.context
    10.7 -  val restricted_scope: Binding.scope -> Proof.context -> Proof.context
    10.8 -  val restricted: Position.T -> Proof.context -> Proof.context
    10.9 +  val qualified_scope: Binding.scope -> Proof.context -> Proof.context
   10.10 +  val qualified: Position.T -> Proof.context -> Proof.context
   10.11    val concealed: Proof.context -> Proof.context
   10.12    val class_space: Proof.context -> Name_Space.T
   10.13    val type_space: Proof.context -> Name_Space.T
   10.14 @@ -321,8 +321,8 @@
   10.15  
   10.16  val private_scope = map_naming o Name_Space.private_scope;
   10.17  val private = map_naming o Name_Space.private;
   10.18 -val restricted_scope = map_naming o Name_Space.restricted_scope;
   10.19 -val restricted = map_naming o Name_Space.restricted;
   10.20 +val qualified_scope = map_naming o Name_Space.qualified_scope;
   10.21 +val qualified = map_naming o Name_Space.qualified;
   10.22  
   10.23  val concealed = map_naming Name_Space.concealed;
   10.24  
    11.1 --- a/src/Pure/Isar/token.ML	Thu Apr 09 18:46:16 2015 +0200
    11.2 +++ b/src/Pure/Isar/token.ML	Thu Apr 09 20:42:38 2015 +0200
    11.3 @@ -247,7 +247,7 @@
    11.4  fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
    11.5    | keyword_with _ _ = false;
    11.6  
    11.7 -val is_command_modifier = keyword_with (fn x => x = "private" orelse x = "restricted");
    11.8 +val is_command_modifier = keyword_with (fn x => x = "private" orelse x = "qualified");
    11.9  
   11.10  fun ident_with pred (Token (_, (Ident, x), _)) = pred x
   11.11    | ident_with _ _ = false;
    12.1 --- a/src/Pure/Isar/token.scala	Thu Apr 09 18:46:16 2015 +0200
    12.2 +++ b/src/Pure/Isar/token.scala	Thu Apr 09 20:42:38 2015 +0200
    12.3 @@ -260,7 +260,7 @@
    12.4    def is_end: Boolean = is_command && source == "end"
    12.5  
    12.6    def is_command_modifier: Boolean =
    12.7 -    is_keyword && (source == "private" || source == "restricted")
    12.8 +    is_keyword && (source == "private" || source == "qualified")
    12.9  
   12.10    def is_begin_block: Boolean = is_command && source == "{"
   12.11    def is_end_block: Boolean = is_command && source == "}"
    13.1 --- a/src/Pure/Isar/toplevel.ML	Thu Apr 09 18:46:16 2015 +0200
    13.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Apr 09 20:42:38 2015 +0200
    13.3 @@ -412,15 +412,16 @@
    13.4          | NONE => raise UNDEF)
    13.5      | _ => raise UNDEF));
    13.6  
    13.7 -val limited_context =
    13.8 -  fn SOME (strict, scope) => Proof_Context.map_naming (Name_Space.limited strict scope) | NONE => I;
    13.9 +fun restricted_context (SOME (strict, scope)) =
   13.10 +      Proof_Context.map_naming (Name_Space.restricted strict scope)
   13.11 +  | restricted_context NONE = I;
   13.12  
   13.13 -fun local_theory' limited target f = present_transaction (fn int =>
   13.14 +fun local_theory' restricted target f = present_transaction (fn int =>
   13.15    (fn Theory (gthy, _) =>
   13.16          let
   13.17            val (finish, lthy) = Named_Target.switch target gthy;
   13.18            val lthy' = lthy
   13.19 -            |> limited_context limited
   13.20 +            |> restricted_context restricted
   13.21              |> Local_Theory.new_group
   13.22              |> f int
   13.23              |> Local_Theory.reset_group;
   13.24 @@ -428,7 +429,7 @@
   13.25      | _ => raise UNDEF))
   13.26    (K ());
   13.27  
   13.28 -fun local_theory limited target f = local_theory' limited target (K f);
   13.29 +fun local_theory restricted target f = local_theory' restricted target (K f);
   13.30  
   13.31  fun present_local_theory target = present_transaction (fn int =>
   13.32    (fn Theory (gthy, _) =>
   13.33 @@ -473,18 +474,18 @@
   13.34  
   13.35  in
   13.36  
   13.37 -fun local_theory_to_proof' limited target f = begin_proof
   13.38 +fun local_theory_to_proof' restricted target f = begin_proof
   13.39    (fn int => fn gthy =>
   13.40      let
   13.41        val (finish, lthy) = Named_Target.switch target gthy;
   13.42        val prf = lthy
   13.43 -        |> limited_context limited
   13.44 +        |> restricted_context restricted
   13.45          |> Local_Theory.new_group
   13.46          |> f int;
   13.47      in (finish o Local_Theory.reset_group, prf) end);
   13.48  
   13.49 -fun local_theory_to_proof limited target f =
   13.50 -  local_theory_to_proof' limited target (K f);
   13.51 +fun local_theory_to_proof restricted target f =
   13.52 +  local_theory_to_proof' restricted target (K f);
   13.53  
   13.54  fun theory_to_proof f = begin_proof
   13.55    (fn _ => fn gthy =>
    14.1 --- a/src/Pure/Pure.thy	Thu Apr 09 18:46:16 2015 +0200
    14.2 +++ b/src/Pure/Pure.thy	Thu Apr 09 20:42:38 2015 +0200
    14.3 @@ -11,7 +11,7 @@
    14.4      "\<subseteq>" "]" "assumes" "attach" "binder" "constrains"
    14.5      "defines" "fixes" "for" "identifier" "if" "in" "includes" "infix"
    14.6      "infixl" "infixr" "is" "notes" "obtains" "open" "output"
    14.7 -    "overloaded" "pervasive" "private" "restricted" "shows"
    14.8 +    "overloaded" "pervasive" "private" "qualified" "shows"
    14.9      "structure" "unchecked" "where" "|"
   14.10    and "text" "txt" :: document_body
   14.11    and "text_raw" :: document_raw
    15.1 --- a/src/Pure/sign.ML	Thu Apr 09 18:46:16 2015 +0200
    15.2 +++ b/src/Pure/sign.ML	Thu Apr 09 20:42:38 2015 +0200
    15.3 @@ -113,6 +113,8 @@
    15.4    val local_path: theory -> theory
    15.5    val private_scope: Binding.scope -> theory -> theory
    15.6    val private: Position.T -> theory -> theory
    15.7 +  val qualified_scope: Binding.scope -> theory -> theory
    15.8 +  val qualified: Position.T -> theory -> theory
    15.9    val concealed: theory -> theory
   15.10    val hide_class: bool -> string -> theory -> theory
   15.11    val hide_type: bool -> string -> theory -> theory
   15.12 @@ -525,8 +527,8 @@
   15.13  
   15.14  val private_scope = map_naming o Name_Space.private_scope;
   15.15  val private = map_naming o Name_Space.private;
   15.16 -val restricted_scope = map_naming o Name_Space.restricted_scope;
   15.17 -val restricted = map_naming o Name_Space.restricted;
   15.18 +val qualified_scope = map_naming o Name_Space.qualified_scope;
   15.19 +val qualified = map_naming o Name_Space.qualified;
   15.20  val concealed = map_naming Name_Space.concealed;
   15.21  
   15.22