# HG changeset patch
# User wenzelm
# Date 1427920841 -7200
# Node ID 9d70a39d1cf30287864cf198cd4470aaf06cb455
# Parent  2d929c17828389227d611496fb4683fcff2d6ce6# Parent  6afbe5a9913942c2f676a4f92dff5b938d46eb48
merged

diff -r 2d929c178283 -r 9d70a39d1cf3 NEWS
--- a/NEWS	Wed Apr 01 19:17:41 2015 +0200
+++ b/NEWS	Wed Apr 01 22:40:41 2015 +0200
@@ -6,6 +6,9 @@
 
 *** General ***
 
+* Command 'experiment' opens an anonymous locale context with private
+naming policy.
+
 * Structural composition of proof methods (meth1; meth2) in Isar
 corresponds to (tac1 THEN_ALL_NEW tac2) in ML.
 
@@ -340,6 +343,14 @@
 
 *** ML ***
 
+* Subtle change of name space policy: undeclared entries are now
+considered inaccessible, instead of accessible via the fully-qualified
+internal name. This mainly affects Name_Space.intern (and derivatives),
+which may produce an unexpected Long_Name.hidden prefix. Note that
+contempory applications use the strict Name_Space.check (and
+derivatives) instead, which is not affected by the change. Potential
+INCOMPATIBILITY in rare applications of Name_Space.intern.
+
 * The main operations to certify logical entities are Thm.ctyp_of and
 Thm.cterm_of with a local context; old-style global theory variants are
 available as Thm.global_ctyp_of and Thm.global_cterm_of.
@@ -407,6 +418,8 @@
 * The Isabelle tool "update_cartouches" changes theory files to use
 cartouches instead of old-style {* verbatim *} or `alt_string` tokens.
 
+* The Isabelle tool "build" provides new options -k and -x.
+
 
 
 New in Isabelle2014 (August 2014)
diff -r 2d929c178283 -r 9d70a39d1cf3 lib/Tools/build
--- a/lib/Tools/build	Wed Apr 01 19:17:41 2015 +0200
+++ b/lib/Tools/build	Wed Apr 01 22:40:41 2015 +0200
@@ -34,11 +34,13 @@
   echo "    -d DIR       include session directory"
   echo "    -g NAME      select session group NAME"
   echo "    -j INT       maximum number of parallel jobs (default 1)"
+  echo "    -k KEYWORD   check theory sources for conflicts with proposed keywords"
   echo "    -l           list session source files"
   echo "    -n           no build -- test dependencies only"
   echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
   echo "    -s           system build mode: produce output in ISABELLE_HOME"
   echo "    -v           verbose"
+  echo "    -x SESSION   exclude SESSION and all its descendants"
   echo
   echo "  Build and manage Isabelle sessions, depending on implicit"
   show_settings "  "
@@ -68,13 +70,15 @@
 declare -a INCLUDE_DIRS=()
 declare -a SESSION_GROUPS=()
 MAX_JOBS=1
+declare -a CHECK_KEYWORDS=()
 LIST_FILES=false
 NO_BUILD=false
 eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
 SYSTEM_MODE=false
 VERBOSE=false
+declare -a EXCLUDE_SESSIONS=()
 
-while getopts "D:Rabcd:g:j:lno:sv" OPT
+while getopts "D:Rabcd:g:j:k:lno:svx:" OPT
 do
   case "$OPT" in
     D)
@@ -102,6 +106,9 @@
       check_number "$OPTARG"
       MAX_JOBS="$OPTARG"
       ;;
+    k)
+      CHECK_KEYWORDS["${#CHECK_KEYWORDS[@]}"]="$OPTARG"
+      ;;
     l)
       LIST_FILES="true"
       ;;
@@ -117,6 +124,9 @@
     v)
       VERBOSE="true"
       ;;
+    x)
+      EXCLUDE_SESSIONS["${#EXCLUDE_SESSIONS[@]}"]="$OPTARG"
+      ;;
     \?)
       usage
       ;;
@@ -145,7 +155,8 @@
   "$REQUIREMENTS" "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \
   "$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
   "${INCLUDE_DIRS[@]}" $'\n' "${SELECT_DIRS[@]}" $'\n' \
-  "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
+  "${SESSION_GROUPS[@]}" $'\n' "${CHECK_KEYWORDS[@]}" $'\n' \
+  "${BUILD_OPTIONS[@]}" $'\n' "${EXCLUDE_SESSIONS[@]}" $'\n' "$@"
 RC="$?"
 
 if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
diff -r 2d929c178283 -r 9d70a39d1cf3 lib/Tools/scala
--- a/lib/Tools/scala	Wed Apr 01 19:17:41 2015 +0200
+++ b/lib/Tools/scala	Wed Apr 01 22:40:41 2015 +0200
@@ -6,6 +6,12 @@
 
 isabelle_admin_build jars || exit $?
 
-isabelle_scala scala -Dfile.encoding=UTF-8 \
+declare -a JAVA_ARGS; eval "JAVA_ARGS=($ISABELLE_JAVA_SYSTEM_OPTIONS)"
+declare -a SCALA_ARGS=()
+for ARG in "${JAVA_ARGS[@]}"
+do
+  SCALA_ARGS["${#SCALA_ARGS[@]}"]="-J$ARG"
+done
+
+isabelle_scala scala "${SCALA_ARGS[@]}" \
   -classpath "$(jvmpath "$ISABELLE_CLASSPATH")" "$@"
-
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Doc/Implementation/Logic.thy	Wed Apr 01 22:40:41 2015 +0200
@@ -982,7 +982,7 @@
 theorem (in empty) false: False
   using bad by blast
 
-ML \<open>@{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])\<close>
+ML_val \<open>@{assert} (Thm.extra_shyps @{thm false} = [@{sort empty}])\<close>
 
 text \<open>Thanks to the inference kernel managing sort hypothesis
   according to their logical significance, this example is merely an
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Doc/Implementation/ML.thy	Wed Apr 01 22:40:41 2015 +0200
@@ -736,7 +736,7 @@
 text %mlex \<open>The following artificial examples show how to produce
   adhoc output of ML values for debugging purposes.\<close>
 
-ML \<open>
+ML_val \<open>
   val x = 42;
   val y = true;
 
@@ -928,7 +928,7 @@
   list.
 \<close>
 
-ML \<open>
+ML_val \<open>
   val s =
     Buffer.empty
     |> Buffer.add "digits: "
@@ -1093,6 +1093,25 @@
     "The frumious Bandersnatch!"]);
 \<close>
 
+text \<open>
+  \medskip An alternative is to make a paragraph of freely-floating words as
+  follows.
+\<close>
+
+ML_command \<open>
+  warning (Pretty.string_of (Pretty.para
+    "Beware the Jabberwock, my son! \
+    \The jaws that bite, the claws that catch! \
+    \Beware the Jubjub Bird, and shun \
+    \The frumious Bandersnatch!"))
+\<close>
+
+text \<open>
+  This has advantages with variable window / popup sizes, but might make it
+  harder to search for message content systematically, e.g.\ by other tools or
+  by humans expecting the ``verse'' of a formal message in a fixed layout.
+\<close>
+
 
 section \<open>Exceptions \label{sec:exceptions}\<close>
 
@@ -1551,7 +1570,7 @@
   prevented.
 \<close>
 
-ML \<open>
+ML_val \<open>
   val items = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10];
 
   val list1 = fold cons items [];
@@ -1564,7 +1583,7 @@
 text \<open>The subsequent example demonstrates how to \emph{merge} two
   lists in a natural way.\<close>
 
-ML \<open>
+ML_val \<open>
   fun merge_lists eq (xs, ys) = fold_rev (insert eq) ys xs;
 \<close>
 
@@ -1817,7 +1836,7 @@
   temporary file names.
 \<close>
 
-ML \<open>
+ML_val \<open>
   val tmp1 = File.tmp_path (Path.basic ("foo" ^ serial_string ()));
   val tmp2 = File.tmp_path (Path.basic ("foo" ^ serial_string ()));
   @{assert} (tmp1 <> tmp2);
@@ -1878,7 +1897,7 @@
   positive integers that are unique over the runtime of the Isabelle
   process:\<close>
 
-ML \<open>
+ML_val \<open>
   local
     val counter = Synchronized.var "counter" 0;
   in
@@ -1888,9 +1907,7 @@
           let val j = i + 1
           in SOME (j, j) end);
   end;
-\<close>
-
-ML \<open>
+
   val a = next ();
   val b = next ();
   @{assert} (a <> b);
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Doc/Implementation/Prelim.thy
--- a/src/Doc/Implementation/Prelim.thy	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Doc/Implementation/Prelim.thy	Wed Apr 01 22:40:41 2015 +0200
@@ -501,6 +501,9 @@
   value can be modified within Isar text like this:
 \<close>
 
+experiment
+begin
+
 declare [[show_types = false]]
   -- \<open>declaration within (local) theory context\<close>
 
@@ -516,6 +519,8 @@
     ..
 end
 
+end
+
 text \<open>Configuration options that are not set explicitly hold a
   default value that can depend on the application context.  This
   allows to retrieve the value from another slot within the context,
@@ -720,7 +725,7 @@
 text %mlex \<open>The following simple examples demonstrate how to produce
   fresh names from the initial @{ML Name.context}.\<close>
 
-ML \<open>
+ML_val \<open>
   val list1 = Name.invent Name.context "a" 5;
   @{assert} (list1 = ["a", "b", "c", "d", "e"]);
 
@@ -732,10 +737,10 @@
 text \<open>\medskip The same works relatively to the formal context as
   follows.\<close>
 
-locale ex = fixes a b c :: 'a
+experiment fixes a b c :: 'a
 begin
 
-ML \<open>
+ML_val \<open>
   val names = Variable.names_of @{context};
 
   val list1 = Name.invent names "a" 5;
@@ -1043,7 +1048,7 @@
   concrete binding inlined into the text:
 \<close>
 
-ML \<open>Binding.pos_of @{binding here}\<close>
+ML_val \<open>Binding.pos_of @{binding here}\<close>
 
 text \<open>\medskip That position can be also printed in a message as
   follows:\<close>
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Doc/Implementation/Proof.thy
--- a/src/Doc/Implementation/Proof.thy	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Doc/Implementation/Proof.thy	Wed Apr 01 22:40:41 2015 +0200
@@ -162,7 +162,7 @@
 text %mlex \<open>The following example shows how to work with fixed term
   and type parameters and with type-inference.\<close>
 
-ML \<open>
+ML_val \<open>
   (*static compile-time context -- for testing only*)
   val ctxt0 = @{context};
 
@@ -188,7 +188,7 @@
   Alternatively, fixed parameters can be renamed explicitly as
   follows:\<close>
 
-ML \<open>
+ML_val \<open>
   val ctxt0 = @{context};
   val ([x1, x2, x3], ctxt1) =
     ctxt0 |> Variable.variant_fixes ["x", "x", "x"];
@@ -325,7 +325,7 @@
   here for testing purposes.
 \<close>
 
-ML \<open>
+ML_val \<open>
   (*static compile-time context -- for testing only*)
   val ctxt0 = @{context};
 
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Doc/Implementation/Tactic.thy
--- a/src/Doc/Implementation/Tactic.thy	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Doc/Implementation/Tactic.thy	Wed Apr 01 22:40:41 2015 +0200
@@ -709,7 +709,7 @@
   \end{warn}
 \<close>
 
-ML \<open>
+ML_val \<open>
   (*BAD -- does not terminate!*)
   fun REPEAT tac = (tac THEN REPEAT tac) ORELSE all_tac;
 \<close>
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Wed Apr 01 22:40:41 2015 +0200
@@ -501,6 +501,7 @@
 text \<open>
   \begin{matharray}{rcl}
     @{command_def "locale"} & : & @{text "theory \<rightarrow> local_theory"} \\
+    @{command_def "experiment"} & : & @{text "theory \<rightarrow> local_theory"} \\
     @{command_def "print_locale"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def "print_locales"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def "locale_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@@ -513,6 +514,8 @@
   @{rail \<open>
     @@{command locale} @{syntax name} ('=' @{syntax locale})? @'begin'?
     ;
+    @@{command experiment} (@{syntax context_elem}*) @'begin'
+    ;
     @@{command print_locale} '!'? @{syntax nameref}
     ;
     @{syntax_def locale}: @{syntax context_elem}+ |
@@ -610,7 +613,12 @@
   @{text "\<Longrightarrow>"} by @{text "\<longrightarrow>"} in HOL; see also
   \secref{sec:object-logic}).  Separate introduction rules @{text
   loc_axioms.intro} and @{text loc.intro} are provided as well.
-  
+
+  \item @{command experiment}~@{text exprs}~@{keyword "begin"} opens an
+  anonymous locale context with private naming policy. Specifications in its
+  body are inaccessible from outside. This is useful to perform experiments,
+  without polluting the name space.
+
   \item @{command "print_locale"}~@{text "locale"} prints the
   contents of the named locale.  The command omits @{element "notes"}
   elements by default.  Use @{command "print_locale"}@{text "!"} to
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Doc/System/Sessions.thy	Wed Apr 01 22:40:41 2015 +0200
@@ -284,11 +284,13 @@
     -d DIR       include session directory
     -g NAME      select session group NAME
     -j INT       maximum number of parallel jobs (default 1)
+    -k KEYWORD   check theory sources for conflicts with proposed keywords
     -l           list session source files
     -n           no build -- test dependencies only
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -s           system build mode: produce output in ISABELLE_HOME
     -v           verbose
+    -x SESSION   exclude SESSION and all its descendants
 
   Build and manage Isabelle sessions, depending on implicit
   ISABELLE_BUILD_OPTIONS="..."
@@ -321,6 +323,10 @@
   The build tool takes session dependencies into account: the set of
   selected sessions is completed by including all ancestors.
 
+  \medskip One or more options @{verbatim "-x"}~@{text SESSION} specify
+  sessions to be excluded. All descendents of excluded sessions are removed
+  from the selection as specified above.
+
   \medskip Option @{verbatim "-R"} reverses the selection in the sense
   that it refers to its requirements: all ancestor sessions excluding
   the original selection.  This allows to prepare the stage for some
@@ -369,7 +375,12 @@
   \medskip Option @{verbatim "-v"} increases the general level of
   verbosity.  Option @{verbatim "-l"} lists the source files that
   contribute to a session.
-\<close>
+
+  \medskip Option @{verbatim "-k"} specifies a newly proposed keyword for
+  outer syntax (multiple uses allowed). The theory sources are checked for
+  conflicts wrt.\ this hypothetical change of syntax, e.g.\ to reveal
+  occurrences of identifiers that need to be quoted.\<close>
+
 
 subsubsection \<open>Examples\<close>
 
diff -r 2d929c178283 -r 9d70a39d1cf3 src/FOL/ex/Locale_Test/Locale_Test1.thy
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Wed Apr 01 22:40:41 2015 +0200
@@ -775,7 +775,7 @@
 
 locale container
 begin
-interpretation private!: roundup True by unfold_locales rule
+interpretation "private"!: roundup True by unfold_locales rule
 lemmas true_copy = private.true
 end
 
diff -r 2d929c178283 -r 9d70a39d1cf3 src/HOL/Bali/WellForm.thy
--- a/src/HOL/Bali/WellForm.thy	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Bali/WellForm.thy	Wed Apr 01 22:40:41 2015 +0200
@@ -1979,7 +1979,7 @@
 
 lemma dynmethd_Object:
   assumes statM: "methd G Object sig = Some statM" and
-        private: "accmodi statM = Private" and 
+        "private": "accmodi statM = Private" and 
        is_cls_C: "is_class G C" and
              wf: "wf_prog G"
   shows "dynmethd G Object C sig = Some statM"
@@ -1992,13 +1992,13 @@
   from wf 
   have is_cls_Obj: "is_class G Object" 
     by simp
-  from statM subclseq is_cls_Obj ws private
+  from statM subclseq is_cls_Obj ws "private"
   show ?thesis
   proof (cases rule: dynmethd_cases)
     case Static then show ?thesis .
   next
     case Overrides 
-    with private show ?thesis 
+    with "private" show ?thesis 
       by (auto dest: no_Private_override)
   qed
 qed
diff -r 2d929c178283 -r 9d70a39d1cf3 src/HOL/Library/Code_Test.thy
--- a/src/HOL/Library/Code_Test.thy	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Library/Code_Test.thy	Wed Apr 01 22:40:41 2015 +0200
@@ -64,7 +64,7 @@
 by(cases x y rule: xml_tree.exhaust[case_product xml_tree.exhaust])(simp)
 
 context begin
-local_setup {* Local_Theory.map_naming (Name_Space.mandatory_path "xml") *}
+local_setup {* Local_Theory.map_background_naming (Name_Space.mandatory_path "xml") *}
 
 type_synonym attributes = "(String.literal \<times> String.literal) list"
 type_synonym body = "xml_tree list"
diff -r 2d929c178283 -r 9d70a39d1cf3 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -529,7 +529,7 @@
 
     val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
       thy3
-      |> Sign.map_naming Name_Space.concealed
+      |> Sign.concealed
       |> Inductive.add_inductive_global
           {quiet_mode = false, verbose = false, alt_name = Binding.name big_rep_name,
            coind = false, no_elim = true, no_ind = false, skip_mono = true}
@@ -1505,7 +1505,7 @@
 
     val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
       thy10
-      |> Sign.map_naming Name_Space.concealed
+      |> Sign.concealed
       |> Inductive.add_inductive_global
           {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
            coind = false, no_elim = false, no_ind = false, skip_mono = true}
diff -r 2d929c178283 -r 9d70a39d1cf3 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Product_Type.thy	Wed Apr 01 22:40:41 2015 +0200
@@ -988,7 +988,7 @@
 context
 begin
 
-local_setup {* Local_Theory.map_naming (Name_Space.mandatory_path "prod") *}
+local_setup {* Local_Theory.map_background_naming (Name_Space.mandatory_path "prod") *}
 
 definition swap :: "'a \<times> 'b \<Rightarrow> 'b \<times> 'a"
 where
diff -r 2d929c178283 -r 9d70a39d1cf3 src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/ROOT	Wed Apr 01 22:40:41 2015 +0200
@@ -706,7 +706,7 @@
     "ex/Measure_Not_CCC"
   document_files "root.tex"
 
-session "HOL-Nominal" (main) in Nominal = HOL +
+session "HOL-Nominal" in Nominal = HOL +
   options [document = false]
   theories Nominal
 
diff -r 2d929c178283 -r 9d70a39d1cf3 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Statespace/state_space.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -173,7 +173,7 @@
 fun mk_free ctxt name =
   if Variable.is_fixed ctxt name orelse Variable.is_declared ctxt name
   then
-    let val n' = Variable.intern_fixed ctxt name
+    let val n' = Variable.intern_fixed ctxt name |> perhaps Long_Name.dest_hidden;
     in SOME (Free (n', Proof_Context.infer_type ctxt (n', dummyT))) end
   else NONE
 
diff -r 2d929c178283 -r 9d70a39d1cf3 src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Wed Apr 01 22:40:41 2015 +0200
@@ -737,16 +737,17 @@
              bnd_def
 
     val thm =
-      if Name_Space.defined_entry (Theory.axiom_space thy) def_name then
-        Thm.axiom thy def_name
-      else
-        if is_none prob_name_opt then
-          (*This mode is for testing, so we can be a bit
-            looser with theories*)
-          Thm.add_axiom_global (bnd_name, conclusion) thy
-          |> fst |> snd
-        else
-          raise (NO_SKOLEM_DEF (def_name, bnd_name, conclusion))
+      (case try (Thm.axiom thy) def_name of
+        SOME thm => thm
+      | NONE =>
+          if is_none prob_name_opt then
+            (*This mode is for testing, so we can be a bit
+              looser with theories*)
+            (* FIXME bad theory context!? *)
+            Thm.add_axiom_global (bnd_name, conclusion) thy
+            |> fst |> snd
+          else
+            raise (NO_SKOLEM_DEF (def_name, bnd_name, conclusion)))
   in
     rtac (Drule.export_without_context thm) i st
   end
diff -r 2d929c178283 -r 9d70a39d1cf3 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -396,9 +396,8 @@
 fun make_class clas = class_prefix ^ ascii_of clas
 
 fun new_skolem_var_name_of_const s =
-  let val ss = s |> space_explode Long_Name.separator in
-    nth ss (length ss - 2)
-  end
+  let val ss = Long_Name.explode s
+  in nth ss (length ss - 2) end
 
 (* These are ignored anyway by the relevance filter (unless they appear in
    higher-order places) but not by the monomorphizer. *)
diff -r 2d929c178283 -r 9d70a39d1cf3 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -414,9 +414,8 @@
     val ps = map (`Long_Name.base_name) names;
     val dups = Library.duplicates (op =) (map fst ps);
     fun underscore s =
-      let val ss = space_explode Long_Name.separator s in
-        space_implode "_" (drop (length ss - 2) ss)
-      end;
+      let val ss = Long_Name.explode s
+      in space_implode "_" (drop (length ss - 2) ss) end;
   in
     map (fn (base, full) => if member (op =) dups base then underscore full else base) ps
     |> Name.variant_list []
diff -r 2d929c178283 -r 9d70a39d1cf3 src/HOL/Tools/BNF/bnf_util.ML
--- a/src/HOL/Tools/BNF/bnf_util.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -145,9 +145,9 @@
     val b' = fold_rev Binding.prefix_name (map (suffix "_" o fst) (Binding.path_of b)) b;
     val ((name, info), (lthy, lthy_old)) =
       lthy
-      |> Local_Theory.concealed
+      |> Proof_Context.concealed
       |> Typedef.add_typedef true (b', Ts, mx) set opt_morphs tac
-      ||> Local_Theory.restore_naming lthy
+      ||> Proof_Context.restore_naming lthy
       ||> `Local_Theory.restore;
     val phi = Proof_Context.export_morphism lthy_old lthy;
   in
diff -r 2d929c178283 -r 9d70a39d1cf3 src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -231,7 +231,7 @@
   | name_noted_thms qualifier base ((local_name, thms) :: noted) =
     if Long_Name.base_name local_name = base then
       (local_name,
-       map_index (uncurry (fn j => Thm.name_derivation (qualifier ^ Long_Name.separator ^ base ^
+       map_index (uncurry (fn j => Thm.name_derivation (Long_Name.append qualifier base ^
          (if can the_single thms then "" else "_" ^ string_of_int (j + 1))))) thms) :: noted
     else
       ((local_name, thms) :: name_noted_thms qualifier base noted);
diff -r 2d929c178283 -r 9d70a39d1cf3 src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -445,7 +445,7 @@
   let
     val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) =
       lthy
-      |> Local_Theory.concealed
+      |> Proof_Context.concealed
       |> Inductive.add_inductive_i
           {quiet_mode = true,
             verbose = ! trace,
@@ -458,7 +458,7 @@
           [] (* no parameters *)
           (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
           [] (* no special monos *)
-      ||> Local_Theory.restore_naming lthy
+      ||> Proof_Context.restore_naming lthy
 
     fun requantify orig_intro thm =
       let
diff -r 2d929c178283 -r 9d70a39d1cf3 src/HOL/Tools/Metis/metis_generate.ML
--- a/src/HOL/Tools/Metis/metis_generate.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Tools/Metis/metis_generate.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -66,8 +66,7 @@
         else metis_ad_hoc_type_tag, true))]
 
 fun old_skolem_const_name i j num_T_args =
-  old_skolem_const_prefix ^ Long_Name.separator ^
-  (space_implode Long_Name.separator (map string_of_int [i, j, num_T_args]))
+  Long_Name.implode (old_skolem_const_prefix :: map string_of_int [i, j, num_T_args])
 
 fun conceal_old_skolem_terms i old_skolems t =
   if exists_Const (curry (op =) @{const_name Meson.skolem} o fst) t then
diff -r 2d929c178283 -r 9d70a39d1cf3 src/HOL/Tools/Old_Datatype/old_datatype.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -172,7 +172,7 @@
 
     val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
       thy1
-      |> Sign.map_naming Name_Space.concealed
+      |> Sign.concealed
       |> Inductive.add_inductive_global
           {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
            coind = false, no_elim = true, no_ind = false, skip_mono = true}
diff -r 2d929c178283 -r 9d70a39d1cf3 src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -146,7 +146,7 @@
 
     val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
       thy0
-      |> Sign.map_naming Name_Space.concealed
+      |> Sign.concealed
       |> Inductive.add_inductive_global
           {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name',
             coind = false, no_elim = false, no_ind = true, skip_mono = true}
diff -r 2d929c178283 -r 9d70a39d1cf3 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -476,7 +476,7 @@
     fun add_facts global foldx facts =
       foldx (fn (name0, ths) => fn accum =>
         if name0 <> "" andalso
-           (Long_Name.is_hidden (Facts.intern facts name0) orelse
+           (is_some (Long_Name.dest_hidden (Facts.intern facts name0)) orelse
             ((Facts.is_concealed facts name0 orelse
               (not generous andalso is_blacklisted_or_something name0)) andalso
              forall (not o member Thm.eq_thm_prop add_ths) ths)) then
diff -r 2d929c178283 -r 9d70a39d1cf3 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -737,8 +737,6 @@
 
 (*** Isabelle helpers ***)
 
-val local_prefix = "local" ^ Long_Name.separator
-
 fun elided_backquote_thm threshold th =
   elide_string threshold (backquote_thm (Proof_Context.init_global (Thm.theory_of_thm th)) th)
 
@@ -748,10 +746,8 @@
   if Thm.has_name_hint th then
     let val hint = Thm.get_name_hint th in
       (* There must be a better way to detect local facts. *)
-      (case try (unprefix local_prefix) hint of
-        SOME suf =>
-        thy_name_of_thm th ^ Long_Name.separator ^ suf ^ Long_Name.separator ^
-        elided_backquote_thm 50 th
+      (case Long_Name.dest_local hint of
+        SOME suf => Long_Name.implode [thy_name_of_thm th, suf, elided_backquote_thm 50 th]
       | NONE => hint)
     end
   else
@@ -886,7 +882,7 @@
       | pattify_term _ _ (Free (s, T)) =
         maybe_singleton_str pat_var_prefix (crude_str_of_typ T)
         |> (if member (op =) fixes s then
-              cons (free_feature_of (massage_long_name (thy_name ^ Long_Name.separator ^ s)))
+              cons (free_feature_of (massage_long_name (Long_Name.append thy_name s)))
             else
               I)
       | pattify_term _ _ (Var (_, T)) = maybe_singleton_str pat_var_prefix (crude_str_of_typ T)
diff -r 2d929c178283 -r 9d70a39d1cf3 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Tools/inductive.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -843,13 +843,13 @@
 
     val is_auxiliary = length cs >= 2; 
     val ((rec_const, (_, fp_def)), lthy') = lthy
-      |> is_auxiliary ? Local_Theory.concealed
+      |> is_auxiliary ? Proof_Context.concealed
       |> Local_Theory.define
         ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
          ((Binding.concealed (Thm.def_binding rec_name), @{attributes [nitpick_unfold]}),
            fold_rev lambda params
              (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
-      ||> is_auxiliary ? Local_Theory.restore_naming lthy;
+      ||> Proof_Context.restore_naming lthy;
     val fp_def' =
       Simplifier.rewrite (put_simpset HOL_basic_ss lthy' addsimps [fp_def])
         (Thm.cterm_of lthy' (list_comb (rec_const, params)));
diff -r 2d929c178283 -r 9d70a39d1cf3 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -488,13 +488,13 @@
 
     (* define inductive sets using previously defined predicates *)
     val (defs, lthy2) = lthy1
-      |> Local_Theory.concealed  (* FIXME ?? *)
+      |> Proof_Context.concealed  (* FIXME ?? *)
       |> fold_map Local_Theory.define
         (map (fn (((c, syn), (fs, U, _)), p) => ((c, syn), ((Thm.def_binding c, []),
            fold_rev lambda params (HOLogic.Collect_const U $
              HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
            (cnames_syn ~~ cs_info ~~ preds))
-      ||> Local_Theory.restore_naming lthy1;
+      ||> Proof_Context.restore_naming lthy1;
 
     (* prove theorems for converting predicate to set notation *)
     val lthy3 = fold
diff -r 2d929c178283 -r 9d70a39d1cf3 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/HOL/Tools/typedef.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -81,10 +81,10 @@
   Typedef_Plugin.interpretation typedef_plugin
     (fn name => fn lthy =>
       lthy
-      |> Local_Theory.map_naming
+      |> Local_Theory.map_background_naming
           (Name_Space.root_path #> Name_Space.add_path (Long_Name.qualifier name))
       |> f name
-      |> Local_Theory.restore_naming lthy);
+      |> Local_Theory.restore_background_naming lthy);
 
 
 (* primitive typedef axiomatization -- for fresh typedecl *)
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/General/binding.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -9,8 +9,9 @@
 
 signature BINDING =
 sig
+  eqtype scope
+  val new_scope: unit -> scope
   eqtype binding
-  val dest: binding -> {private: bool, concealed: bool, path: (string * bool) list, name: bstring}
   val path_of: binding -> (string * bool) list
   val make: bstring * Position.T -> binding
   val pos_of: binding -> Position.T
@@ -29,13 +30,16 @@
   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: binding -> binding
+  val private: scope -> binding -> binding
+  val private_default: scope option -> binding -> binding
   val concealed: binding -> binding
   val pretty: binding -> Pretty.T
   val print: binding -> string
   val pp: binding -> Pretty.T
   val bad: binding -> string
   val check: binding -> unit
+  val name_spec: scope list -> (string * bool) list -> binding ->
+    {accessible: bool, concealed: bool, spec: (string * bool) list}
 end;
 
 structure Binding: BINDING =
@@ -43,10 +47,17 @@
 
 (** representation **)
 
-(* datatype *)
+(* scope of private entries *)
+
+datatype scope = Scope of serial;
+
+fun new_scope () = Scope (serial ());
+
+
+(* binding *)
 
 datatype binding = Binding of
- {private: bool,                    (*entry is strictly private -- no name space accesses*)
+ {private: scope option,            (*entry is strictly private within its scope*)
   concealed: bool,                  (*entry is for foundational purposes -- please ignore*)
   prefix: (string * bool) list,     (*system prefix*)
   qualifier: (string * bool) list,  (*user qualifier*)
@@ -60,10 +71,7 @@
 fun map_binding f (Binding {private, concealed, prefix, qualifier, name, pos}) =
   make_binding (f (private, concealed, prefix, qualifier, name, pos));
 
-fun dest (Binding {private, concealed, prefix, qualifier, name, ...}) =
-  {private = private, concealed = concealed, path = prefix @ qualifier, name = name};
-
-val path_of = #path o dest;
+fun path_of (Binding {prefix, qualifier, ...}) = prefix @ qualifier;
 
 
 
@@ -71,7 +79,7 @@
 
 (* name and position *)
 
-fun make (name, pos) = make_binding (false, false, [], [], name, pos);
+fun make (name, pos) = make_binding (NONE, false, [], [], name, pos);
 
 fun pos_of (Binding {pos, ...}) = pos;
 fun set_pos pos =
@@ -109,7 +117,7 @@
 fun qualified_name "" = empty
   | qualified_name s =
       let val (qualifier, name) = split_last (Long_Name.explode s)
-      in make_binding (false, false, [], map (rpair false) qualifier, name, Position.none) end;
+      in make_binding (NONE, false, [], map (rpair false) qualifier, name, Position.none) end;
 
 
 (* system prefix *)
@@ -126,9 +134,13 @@
 
 (* visibility flags *)
 
-val private =
+fun private scope =
   map_binding (fn (_, concealed, prefix, qualifier, name, pos) =>
-    (true, concealed, prefix, qualifier, name, pos));
+    (SOME scope, concealed, prefix, qualifier, name, pos));
+
+fun private_default private' =
+  map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
+    (if is_some private then private else private', concealed, prefix, qualifier, name, pos));
 
 val concealed =
   map_binding (fn (private, _, prefix, qualifier, name, pos) =>
@@ -157,6 +169,31 @@
   if Symbol_Pos.is_identifier (name_of binding) then ()
   else legacy_feature (bad binding);
 
+
+
+(** resulting name_spec **)
+
+val bad_specs = ["", "??", "__"];
+
+fun name_spec scopes path binding =
+  let
+    val Binding {private, concealed, prefix, qualifier, name, ...} = binding;
+    val _ = Long_Name.is_qualified name andalso error (bad binding);
+
+    val accessible =
+      (case private of
+        NONE => true
+      | SOME scope => member (op =) scopes scope);
+
+    val spec1 =
+      maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix @ qualifier);
+    val spec2 = if name = "" then [] else [(name, true)];
+    val spec = spec1 @ spec2;
+    val _ =
+      exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
+      andalso error (bad binding);
+  in {accessible = accessible, concealed = concealed, spec = if null spec2 then [] else spec} end;
+
 end;
 
 type binding = Binding.binding;
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Pure/General/long_name.ML
--- a/src/Pure/General/long_name.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/General/long_name.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -9,9 +9,9 @@
   val separator: string
   val is_qualified: string -> bool
   val hidden: string -> string
-  val is_hidden: string -> bool
+  val dest_hidden: string -> string option
   val localN: string
-  val is_local: string -> bool
+  val dest_local: string -> string option
   val implode: string list -> string
   val explode: string -> string list
   val append: string -> string -> string
@@ -29,11 +29,11 @@
 
 val is_qualified = exists_string (fn s => s = separator);
 
-fun hidden name = "??." ^ name;
-val is_hidden = String.isPrefix "??.";
+val hidden = prefix "??.";
+val dest_hidden = try (unprefix "??.");
 
 val localN = "local";
-val is_local = String.isPrefix "local.";
+val dest_local = try (unprefix "local.");
 
 val implode = space_implode separator;
 val explode = space_explode separator;
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/General/name_space.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -12,11 +12,10 @@
   type T
   val empty: string -> T
   val kind_of: T -> string
-  val defined_entry: T -> string -> bool
+  val markup: T -> string -> Markup.T
   val the_entry: T -> string ->
     {concealed: bool, group: serial option, theory_name: string, pos: Position.T, serial: serial}
   val entry_ord: T -> string * string -> order
-  val markup: T -> string -> Markup.T
   val is_concealed: T -> string -> bool
   val intern: T -> xstring -> string
   val names_long_raw: Config.raw
@@ -33,7 +32,9 @@
   val completion: Context.generic -> T -> xstring * Position.T -> Completion.T
   val merge: T * T -> T
   type naming
-  val private: naming -> naming
+  val get_scope: naming -> Binding.scope option
+  val new_scope: naming -> Binding.scope * naming
+  val private: Binding.scope -> naming -> naming
   val concealed: naming -> naming
   val get_group: naming -> serial option
   val set_group: serial option -> naming -> naming
@@ -47,6 +48,7 @@
   val qualified_path: bool -> binding -> naming -> naming
   val global_naming: naming
   val local_naming: naming
+  val transform_naming: naming -> naming -> naming
   val transform_binding: naming -> binding -> binding
   val full_name: naming -> binding -> string
   val base_name: binding -> string
@@ -62,6 +64,8 @@
   val check_reports: Context.generic -> 'a table ->
     xstring * Position.T list -> (string * Position.report list) * 'a
   val check: Context.generic -> 'a table -> xstring * Position.T -> string * 'a
+  val defined: 'a table -> string -> bool
+  val lookup: 'a table -> string -> 'a option
   val lookup_key: 'a table -> string -> (string * 'a) option
   val get: 'a table -> string -> 'a
   val define: Context.generic -> bool -> binding * 'a -> 'a table -> string * 'a table
@@ -105,12 +109,10 @@
   error ("Duplicate " ^ plain_words kind ^ " declaration " ^
     print_entry_ref kind entry1 ^ " vs. " ^ print_entry_ref kind entry2 ^ Position.here pos);
 
-fun undefined kind name = "Undefined " ^ plain_words kind ^ ": " ^ quote name;
-
 
 (* internal names *)
 
-type internals = (string list * string list) Change_Table.T;  (*xname -> visible, hidden*)
+type internals = (string list * string list) Change_Table.T;
 
 fun map_internals f xname : internals -> internals =
   Change_Table.map_default (xname, ([], [])) f;
@@ -119,14 +121,15 @@
 fun del_name_extra name =
   map_internals (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
 val add_name = map_internals o apfst o update (op =);
-val add_name' = map_internals o apsnd o update (op =);
+fun hide_name name = map_internals (apsnd (update (op =) name)) name;
 
 
 (* datatype T *)
 
 datatype T =
   Name_Space of
-   {kind: string, internals: internals,
+   {kind: string,
+    internals: internals,  (*xname -> visible, hidden*)
     entries: (xstring list * entry) Change_Table.T};  (*name -> externals, entry*)
 
 fun make_name_space (kind, internals, entries) =
@@ -146,36 +149,46 @@
 
 fun kind_of (Name_Space {kind, ...}) = kind;
 
-fun defined_entry (Name_Space {entries, ...}) = Change_Table.defined entries;
-
-fun the_entry (Name_Space {kind, entries, ...}) name =
-  (case Change_Table.lookup entries name of
-    NONE => error (undefined kind name)
-  | SOME (_, entry) => entry);
-
-fun entry_ord space = int_ord o apply2 (#serial o the_entry space);
-
 fun markup (Name_Space {kind, entries, ...}) name =
   (case Change_Table.lookup entries name of
     NONE => Markup.intensify
   | SOME (_, entry) => entry_markup false kind (name, entry));
 
+fun undefined (space as Name_Space {kind, entries, ...}) bad =
+  let
+    val (prfx, sfx) =
+      (case Long_Name.dest_hidden bad of
+        SOME name =>
+          if Change_Table.defined entries name
+          then ("Inaccessible", Markup.markup (markup space name) (quote name))
+          else ("Undefined", quote name)
+      | NONE => ("Undefined", quote bad));
+  in prfx ^ " " ^ plain_words kind ^ ": " ^ sfx end;
+
+fun the_entry (space as Name_Space {entries, ...}) name =
+  (case Change_Table.lookup entries name of
+    NONE => error (undefined space name)
+  | SOME (_, entry) => entry);
+
+fun entry_ord space = int_ord o apply2 (#serial o the_entry space);
+
 fun is_concealed space name = #concealed (the_entry space name);
 
 
-(* name accesses *)
+(* intern *)
 
-fun lookup (Name_Space {internals, ...}) xname =
-  (case Change_Table.lookup internals xname of
-    NONE => (xname, true)
-  | SOME ([], []) => (xname, true)
-  | SOME ([name], _) => (name, true)
-  | SOME (name :: _, _) => (name, false)
-  | SOME ([], name' :: _) => (Long_Name.hidden name', true));
+fun intern' (Name_Space {internals, ...}) xname =
+  (case the_default ([], []) (Change_Table.lookup internals xname) of
+    ([name], _) => (name, true)
+  | (name :: _, _) => (name, false)
+  | ([], []) => (Long_Name.hidden xname, true)
+  | ([], name' :: _) => (Long_Name.hidden name', true));
+
+val intern = #1 oo intern';
 
 fun get_accesses (Name_Space {entries, ...}) name =
   (case Change_Table.lookup entries name of
-    NONE => [name]
+    NONE => []
   | SOME (externals, _) => externals);
 
 fun valid_accesses (Name_Space {internals, ...}) name =
@@ -183,11 +196,6 @@
     if not (null names) andalso hd names = name then cons xname else I) internals [];
 
 
-(* intern *)
-
-fun intern space xname = #1 (lookup space xname);
-
-
 (* extern *)
 
 val names_long_raw = Config.declare_option ("names_long", @{here});
@@ -206,7 +214,7 @@
     val names_unique = Config.get ctxt names_unique;
 
     fun valid require_unique xname =
-      let val (name', is_unique) = lookup space xname
+      let val (name', is_unique) = intern' space xname
       in name = name' andalso (not require_unique orelse is_unique) end;
 
     fun ext [] = if valid false name then name else Long_Name.hidden name
@@ -236,7 +244,7 @@
   Completion.make (xname, pos) (fn completed =>
     let
       fun result_ord ((xname1, (_, name1)), (xname2, (_, name2))) =
-        (case bool_ord (apply2 Long_Name.is_local (name2, name1)) of
+        (case bool_ord (apply2 (is_some o Long_Name.dest_local) (name2, name1)) of
           EQUAL =>
             (case int_ord (apply2 Long_Name.qualification (xname1, xname2)) of
               EQUAL => string_ord (xname1, xname2)
@@ -284,41 +292,54 @@
 (* datatype naming *)
 
 datatype naming = Naming of
- {private: bool,
+ {scopes: Binding.scope list,
+  private: Binding.scope option,
   concealed: bool,
   group: serial option,
   theory_name: string,
   path: (string * bool) list};
 
-fun make_naming (private, concealed, group, theory_name, path) =
-  Naming {private = private, concealed = concealed, group = group,
-    theory_name = theory_name, path = path};
+fun make_naming (scopes, private, concealed, group, theory_name, path) =
+  Naming {scopes = scopes, private = private, concealed = concealed,
+    group = group, theory_name = theory_name, path = path};
 
-fun map_naming f (Naming {private, concealed, group, theory_name, path}) =
-  make_naming (f (private, concealed, group, theory_name, path));
+fun map_naming f (Naming {scopes, private, concealed, group, theory_name, path}) =
+  make_naming (f (scopes, private, concealed, group, theory_name, path));
 
-fun map_path f = map_naming (fn (private, concealed, group, theory_name, path) =>
-  (private, concealed, group, theory_name, f path));
+fun map_path f = map_naming (fn (scopes, private, concealed, group, theory_name, path) =>
+  (scopes, private, concealed, group, theory_name, f path));
 
 
-val private = map_naming (fn (_, concealed, group, theory_name, path) =>
-  (true, concealed, group, theory_name, path));
+fun get_scopes (Naming {scopes, ...}) = scopes;
+val get_scope = try hd o get_scopes;
 
-val concealed = map_naming (fn (private, _, group, theory_name, path) =>
-  (private, true, group, theory_name, path));
+fun new_scope naming =
+  let
+    val scope = Binding.new_scope ();
+    val naming' =
+      naming |> map_naming (fn (scopes, private, concealed, group, theory_name, path) =>
+        (scope :: scopes, private, concealed, group, theory_name, path));
+  in (scope, naming') end;
 
-fun set_theory_name theory_name = map_naming (fn (private, concealed, group, _, path) =>
-  (private, concealed, group, theory_name, path));
+fun private scope = map_naming (fn (scopes, _, concealed, group, theory_name, path) =>
+  (scopes, SOME scope, concealed, group, theory_name, path));
 
+val concealed = map_naming (fn (scopes, private, _, group, theory_name, path) =>
+  (scopes, private, true, group, theory_name, path));
+
+fun set_theory_name theory_name = map_naming (fn (scopes, private, concealed, group, _, path) =>
+  (scopes, private, concealed, group, theory_name, path));
 
 fun get_group (Naming {group, ...}) = group;
 
-fun set_group group = map_naming (fn (private, concealed, _, theory_name, path) =>
-  (private, concealed, group, theory_name, path));
+fun set_group group = map_naming (fn (scopes, private, concealed, _, theory_name, path) =>
+  (scopes, private, concealed, group, theory_name, path));
 
 fun new_group naming = set_group (SOME (serial ())) naming;
 val reset_group = set_group NONE;
 
+fun get_path (Naming {path, ...}) = path;
+
 fun add_path elems = map_path (fn path => path @ [(elems, false)]);
 val root_path = map_path (fn _ => []);
 val parent_path = map_path (perhaps (try (#1 o split_last)));
@@ -327,33 +348,25 @@
 fun qualified_path mandatory binding = map_path (fn path =>
   path @ Binding.path_of (Binding.qualified mandatory "" binding));
 
-val global_naming = make_naming (false, false, NONE, "", []);
+val global_naming = make_naming ([], NONE, false, NONE, "", []);
 val local_naming = global_naming |> add_path Long_Name.localN;
 
 
+(* visibility flags *)
+
+fun transform_naming (Naming {private = private', concealed = concealed', ...}) =
+  fold private (the_list private') #>
+  concealed' ? concealed;
+
+fun transform_binding (Naming {private, concealed, ...}) =
+  Binding.private_default private #>
+  concealed ? Binding.concealed;
+
+
 (* full name *)
 
-fun err_bad binding = error (Binding.bad binding);
-
-fun transform_binding (Naming {private, concealed, ...}) =
-  private ? Binding.private #>
-  concealed ? Binding.concealed;
-
-val bad_specs = ["", "??", "__"];
-
-fun name_spec (naming as Naming {path = path1, ...}) raw_binding =
-  let
-    val binding = transform_binding naming raw_binding;
-    val {private, concealed, path = path2, name} = Binding.dest binding;
-    val _ = Long_Name.is_qualified name andalso err_bad binding;
-
-    val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path1 @ path2);
-    val spec2 = if name = "" then [] else [(name, true)];
-    val spec = spec1 @ spec2;
-    val _ =
-      exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
-      andalso err_bad binding;
-  in {private = private, concealed = concealed, spec = if null spec2 then [] else spec} end;
+fun name_spec naming binding =
+  Binding.name_spec (get_scopes naming) (get_path naming) (transform_binding naming binding);
 
 fun full_name naming =
   name_spec naming #> #spec #> map #1 #> Long_Name.implode;
@@ -374,7 +387,7 @@
 
 fun accesses naming binding =
   (case name_spec naming binding of
-    {private = true, ...} => ([], [])
+    {accessible = false, ...} => ([], [])
   | {spec, ...} =>
       let
         val sfxs = mandatory_suffixes spec;
@@ -387,10 +400,10 @@
 fun hide fully name space =
   space |> map_name_space (fn (kind, internals, entries) =>
     let
-      val _ = Change_Table.defined entries name orelse error (undefined kind name);
+      val _ = the_entry space name;
       val names = valid_accesses space name;
       val internals' = internals
-        |> add_name' name name
+        |> hide_name name
         |> fold (del_name name)
           (if fully then names else inter (op =) [Long_Name.base_name name] names)
         |> fold (del_name_extra name) (get_accesses space name);
@@ -402,7 +415,7 @@
 fun alias naming binding name space =
   space |> map_name_space (fn (kind, internals, entries) =>
     let
-      val _ = Change_Table.defined entries name orelse error (undefined kind name);
+      val _ = the_entry space name;
       val (accs, accs') = accesses naming binding;
       val internals' = internals |> fold (add_name name) accs;
       val entries' = entries
@@ -446,7 +459,7 @@
     val (accs, accs') = accesses naming binding;
 
     val name = Long_Name.implode (map fst spec);
-    val _ = name = "" andalso err_bad binding;
+    val _ = name = "" andalso error (Binding.bad binding);
 
     val (proper_pos, pos) = Position.default (Binding.pos_of binding);
     val entry =
@@ -498,7 +511,7 @@
         let
           val completions = map (fn pos => completion context space (xname, pos)) ps;
         in
-          error (undefined (kind_of space) name ^ Position.here_list ps ^
+          error (undefined space name ^ Position.here_list ps ^
             Markup.markup_report (implode (map Completion.reported_text completions)))
         end)
   end;
@@ -509,12 +522,14 @@
     val _ = Position.reports reports;
   in (name, x) end;
 
+fun defined (Table (_, tab)) name = Change_Table.defined tab name;
+fun lookup (Table (_, tab)) name = Change_Table.lookup tab name;
 fun lookup_key (Table (_, tab)) name = Change_Table.lookup_key tab name;
 
 fun get table name =
   (case lookup_key table name of
     SOME (_, x) => x
-  | NONE => error (undefined (kind_of (space_of_table table)) name));
+  | NONE => error (undefined (space_of_table table) name));
 
 fun define context strict (binding, x) (Table (space, tab)) =
   let
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/Isar/bundle.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -20,9 +20,10 @@
   val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
   val including: string list -> Proof.state -> Proof.state
   val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
-  val context: string list -> Element.context_i list -> generic_theory -> local_theory
+  val context: string list -> Element.context_i list ->
+    generic_theory -> Binding.scope * local_theory
   val context_cmd: (xstring * Position.T) list -> Element.context list ->
-    generic_theory -> local_theory
+    generic_theory -> Binding.scope * local_theory
   val print_bundles: Proof.context -> unit
 end;
 
@@ -97,8 +98,8 @@
       |> gen_includes get raw_incls
       |> prep_decl ([], []) I raw_elems;
   in
-    lthy' |> Local_Theory.open_target
-      (Local_Theory.naming_of lthy) (Local_Theory.operations_of lthy) after_close
+    lthy' |> Local_Theory.init_target
+      (Local_Theory.background_naming_of lthy) (Local_Theory.operations_of lthy) after_close
   end;
 
 in
@@ -137,4 +138,3 @@
   end |> Pretty.writeln_chunks;
 
 end;
-
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/Isar/class.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -599,8 +599,6 @@
 
 fun instantiation (tycos, vs, sort) thy =
   let
-    val naming = Sign.naming_of thy;
-
     val _ = if null tycos then error "At least one arity must be given" else ();
     val class_params = these_params thy (filter (can (Axclass.get_info thy)) sort);
     fun get_param tyco (param, (_, (c, ty))) =
@@ -637,7 +635,7 @@
     |> Overloading.activate_improvable_syntax
     |> Context.proof_map (Syntax_Phases.term_check 0 "resorting" resort_check)
     |> synchronize_inst_syntax
-    |> Local_Theory.init naming
+    |> Local_Theory.init (Sign.naming_of thy)
        {define = Generic_Target.define foundation,
         notes = Generic_Target.notes Generic_Target.theory_notes,
         abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Pure/Isar/experiment.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/experiment.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -0,0 +1,29 @@
+(*  Title:      Pure/Isar/experiment.ML
+    Author:     Makarius
+
+Target for specification experiments that are mostly private.
+*)
+
+signature EXPERIMENT =
+sig
+  val experiment: Element.context_i list -> theory -> Binding.scope * local_theory
+  val experiment_cmd: Element.context list -> theory -> Binding.scope * local_theory
+end;
+
+structure Experiment: EXPERIMENT =
+struct
+
+fun gen_experiment add_locale elems thy =
+  let
+    val (_, lthy) = thy
+      |> add_locale (Binding.name ("experiment" ^ serial_string ())) Binding.empty ([], []) elems;
+    val (scope, naming) =
+      Name_Space.new_scope (Proof_Context.naming_of (Local_Theory.target_of lthy));
+    val naming' = naming |> Name_Space.private scope;
+    val lthy' = lthy |> Local_Theory.map_contexts (K (Proof_Context.map_naming (K naming')));
+  in (scope, lthy') end;
+
+val experiment = gen_experiment Expression.add_locale;
+val experiment_cmd = gen_experiment Expression.add_locale_cmd;
+
+end;
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -361,7 +361,7 @@
     ((Parse.position Parse.xname >> (fn name =>
         Toplevel.begin_local_theory true (Named_Target.begin name)) ||
       Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
-        >> (fn (incls, elems) => Toplevel.open_target (Bundle.context_cmd incls elems)))
+        >> (fn (incls, elems) => Toplevel.open_target (#2 o Bundle.context_cmd incls elems)))
       --| Parse.begin);
 
 
@@ -373,13 +373,19 @@
   Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
 
 val _ =
-  Outer_Syntax.command @{command_spec "locale"} "define named proof context"
+  Outer_Syntax.command @{command_spec "locale"} "define named specification context"
     (Parse.binding --
       Scan.optional (@{keyword "="} |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
       >> (fn ((name, (expr, elems)), begin) =>
           Toplevel.begin_local_theory begin
             (Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
 
+val _ =
+  Outer_Syntax.command @{command_spec "experiment"} "open private specification context"
+    (Scan.repeat Parse_Spec.context_element --| Parse.begin
+      >> (fn elems =>
+          Toplevel.begin_local_theory true (Experiment.experiment_cmd elems #> snd)));
+
 fun interpretation_args mandatory =
   Parse.!!! (Parse_Spec.locale_expression mandatory) --
     Scan.optional
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/Isar/local_theory.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -21,17 +21,14 @@
   val assert_bottom: bool -> local_theory -> local_theory
   val mark_brittle: local_theory -> local_theory
   val assert_nonbrittle: local_theory -> local_theory
-  val open_target: Name_Space.naming -> operations -> (local_theory -> local_theory) ->
+  val map_contexts: (int -> Proof.context -> Proof.context) -> local_theory -> local_theory
+  val background_naming_of: local_theory -> Name_Space.naming
+  val map_background_naming: (Name_Space.naming -> Name_Space.naming) ->
     local_theory -> local_theory
-  val close_target: local_theory -> local_theory
-  val map_contexts: (int -> Proof.context -> Proof.context) -> local_theory -> local_theory
-  val naming_of: local_theory -> Name_Space.naming
+  val restore_background_naming: local_theory -> local_theory -> local_theory
   val full_name: local_theory -> binding -> string
-  val map_naming: (Name_Space.naming -> Name_Space.naming) -> local_theory -> local_theory
-  val concealed: local_theory -> local_theory
   val new_group: local_theory -> local_theory
   val reset_group: local_theory -> local_theory
-  val restore_naming: local_theory -> local_theory -> local_theory
   val standard_morphism: local_theory -> Proof.context -> morphism
   val standard_form: local_theory -> Proof.context -> (morphism -> 'a) -> 'a
   val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
@@ -73,6 +70,10 @@
   val exit_global: local_theory -> theory
   val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context
   val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory
+  val init_target: Name_Space.naming -> operations -> (local_theory -> local_theory) ->
+    local_theory -> Binding.scope * local_theory
+  val open_target: local_theory -> Binding.scope * local_theory
+  val close_target: local_theory -> local_theory
 end;
 
 structure Local_Theory: LOCAL_THEORY =
@@ -97,15 +98,15 @@
   exit: local_theory -> Proof.context};
 
 type lthy =
- {naming: Name_Space.naming,
+ {background_naming: Name_Space.naming,
   operations: operations,
   after_close: local_theory -> local_theory,
   brittle: bool,
   target: Proof.context};
 
-fun make_lthy (naming, operations, after_close, brittle, target) : lthy =
-  {naming = naming, operations = operations, after_close = after_close,
-    brittle = brittle, target = target};
+fun make_lthy (background_naming, operations, after_close, brittle, target) : lthy =
+  {background_naming = background_naming, operations = operations,
+    after_close = after_close, brittle = brittle, target = target};
 
 
 (* context data *)
@@ -124,8 +125,8 @@
 
 fun map_top f =
   assert #>
-  Data.map (fn {naming, operations, after_close, brittle, target} :: parents =>
-    make_lthy (f (naming, operations, after_close, brittle, target)) :: parents);
+  Data.map (fn {background_naming, operations, after_close, brittle, target} :: parents =>
+    make_lthy (f (background_naming, operations, after_close, brittle, target)) :: parents);
 
 fun restore lthy = #target (top_of lthy) |> Data.put (Data.get lthy);
 
@@ -144,25 +145,16 @@
     else lthy
   end;
 
-fun open_target naming operations after_close target =
-  assert target
-  |> Data.map (cons (make_lthy (naming, operations, after_close, true, target)));
-
-fun close_target lthy =
-  let
-    val _ = assert_bottom false lthy;
-    val ({after_close, ...} :: rest) = Data.get lthy;
-  in lthy |> Data.put rest |> restore |> after_close end;
-
 fun map_contexts f lthy =
   let val n = level lthy in
-    lthy |> (Data.map o map_index) (fn (i, {naming, operations, after_close, brittle, target}) =>
-      make_lthy (naming, operations, after_close, brittle,
-        target
-        |> Context_Position.set_visible false
-        |> f (n - i - 1)
-        |> Context_Position.restore_visible target))
-    |> f n
+    lthy |> (Data.map o map_index)
+      (fn (i, {background_naming, operations, after_close, brittle, target}) =>
+        make_lthy (background_naming, operations, after_close, brittle,
+          target
+          |> Context_Position.set_visible false
+          |> f (n - i - 1)
+          |> Context_Position.restore_visible target))
+      |> f n
   end;
 
 
@@ -170,8 +162,8 @@
 
 fun mark_brittle lthy =
   if level lthy = 1 then
-    map_top (fn (naming, operations, after_close, _, target) =>
-      (naming, operations, after_close, true, target)) lthy
+    map_top (fn (background_naming, operations, after_close, _, target) =>
+      (background_naming, operations, after_close, true, target)) lthy
   else lthy;
 
 fun assert_nonbrittle lthy =
@@ -179,20 +171,20 @@
   else lthy;
 
 
-(* naming *)
+(* naming for background theory *)
 
-val naming_of = #naming o top_of;
-val full_name = Name_Space.full_name o naming_of;
+val background_naming_of = #background_naming o top_of;
 
-fun map_naming f =
-  map_top (fn (naming, operations, after_close, brittle, target) =>
-    (f naming, operations, after_close, brittle, target));
+fun map_background_naming f =
+  map_top (fn (background_naming, operations, after_close, brittle, target) =>
+    (f background_naming, operations, after_close, brittle, target));
 
-val concealed = map_naming Name_Space.concealed;
-val new_group = map_naming Name_Space.new_group;
-val reset_group = map_naming Name_Space.reset_group;
+val restore_background_naming = map_background_naming o K o background_naming_of;
 
-val restore_naming = map_naming o K o naming_of;
+val full_name = Name_Space.full_name o background_naming_of;
+
+val new_group = map_background_naming Name_Space.new_group;
+val reset_group = map_background_naming Name_Space.reset_group;
 
 
 (* standard morphisms *)
@@ -200,7 +192,7 @@
 fun standard_morphism lthy ctxt =
   Proof_Context.norm_export_morphism lthy ctxt $>
   Morphism.binding_morphism "Local_Theory.standard_binding"
-    (Name_Space.transform_binding (naming_of lthy));
+    (Name_Space.transform_binding (Proof_Context.naming_of lthy));
 
 fun standard_form lthy ctxt x =
   Morphism.form (Morphism.transform (standard_morphism lthy ctxt) x);
@@ -217,11 +209,17 @@
 fun raw_theory f = #2 o raw_theory_result (f #> pair ());
 
 fun background_theory_result f lthy =
-  lthy |> raw_theory_result (fn thy =>
-    thy
-    |> Sign.map_naming (K (naming_of lthy))
-    |> f
-    ||> Sign.restore_naming thy);
+  let
+    val naming =
+      background_naming_of lthy
+      |> Name_Space.transform_naming (Proof_Context.naming_of lthy);
+  in
+    lthy |> raw_theory_result (fn thy =>
+      thy
+      |> Sign.map_naming (K naming)
+      |> f
+      ||> Sign.restore_naming thy)
+  end;
 
 fun background_theory f = #2 o background_theory_result (f #> pair ());
 
@@ -339,18 +337,15 @@
 
 
 
-(** init and exit **)
+(** manage targets **)
 
-(* init *)
+(* outermost target *)
 
-fun init naming operations target =
+fun init background_naming operations target =
   target |> Data.map
-    (fn [] => [make_lthy (naming, operations, I, false, target)]
+    (fn [] => [make_lthy (background_naming, operations, I, false, target)]
       | _ => error "Local theory already initialized");
 
-
-(* exit *)
-
 val exit = operation #exit;
 val exit_global = Proof_Context.theory_of o exit;
 
@@ -367,4 +362,25 @@
     val phi = standard_morphism lthy thy_ctxt;
   in (f phi x, thy) end;
 
+
+(* nested targets *)
+
+fun init_target background_naming operations after_close lthy =
+  let
+    val _ = assert lthy;
+    val (scope, target) = Proof_Context.new_scope lthy;
+    val lthy' =
+      target
+      |> Data.map (cons (make_lthy (background_naming, operations, after_close, true, target)));
+  in (scope, lthy') end;
+
+fun open_target lthy =
+  init_target (background_naming_of lthy) (operations_of lthy) I lthy;
+
+fun close_target lthy =
+  let
+    val _ = assert_bottom false lthy;
+    val ({after_close, ...} :: rest) = Data.get lthy;
+  in lthy |> Data.put rest |> restore |> after_close end;
+
 end;
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -180,7 +180,7 @@
 fun markup_name ctxt name = markup_extern ctxt name |-> Markup.markup;
 fun pretty_name ctxt name = markup_extern ctxt name |> Pretty.mark_str;
 
-val get_locale = Option.map #2 oo (Name_Space.lookup_key o Locales.get);
+val get_locale = Name_Space.lookup o Locales.get;
 val defined = is_some oo get_locale;
 
 fun the_locale thy name =
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/Isar/named_target.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -155,14 +155,14 @@
 fun gen_init before_exit target thy =
   let
     val name_data = make_name_data thy target;
-    val naming = Sign.naming_of thy
-      |> Name_Space.mandatory_path (Long_Name.base_name target);
+    val background_naming =
+      Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name target);
   in
     thy
     |> Sign.change_begin
     |> init_context name_data
     |> is_none before_exit ? Data.put (SOME name_data)
-    |> Local_Theory.init naming
+    |> Local_Theory.init background_naming
        {define = Generic_Target.define (foundation name_data),
         notes = Generic_Target.notes (notes name_data),
         abbrev = Generic_Target.abbrev (abbrev name_data),
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/Isar/overloading.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -189,7 +189,6 @@
 fun gen_overloading prep_const raw_overloading thy =
   let
     val ctxt = Proof_Context.init_global thy;
-    val naming = Sign.naming_of thy;
     val _ = if null raw_overloading then error "At least one parameter must be given" else ();
     val overloading = raw_overloading |> map (fn (v, const, checked) =>
       (Term.dest_Const (prep_const ctxt const), (v, checked)));
@@ -201,7 +200,7 @@
     |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
     |> activate_improvable_syntax
     |> synchronize_syntax
-    |> Local_Theory.init naming
+    |> Local_Theory.init (Sign.naming_of thy)
        {define = Generic_Target.define foundation,
         notes = Generic_Target.notes Generic_Target.theory_notes,
         abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -34,6 +34,10 @@
   val naming_of: Proof.context -> Name_Space.naming
   val restore_naming: Proof.context -> Proof.context -> Proof.context
   val full_name: Proof.context -> binding -> string
+  val get_scope: Proof.context -> Binding.scope option
+  val new_scope: Proof.context -> Binding.scope * Proof.context
+  val private: Binding.scope -> 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
   val const_space: Proof.context -> Name_Space.T
@@ -304,6 +308,17 @@
 
 val full_name = Name_Space.full_name o naming_of;
 
+val get_scope = Name_Space.get_scope o naming_of;
+
+fun new_scope ctxt =
+  let
+    val (scope, naming') = Name_Space.new_scope (naming_of ctxt);
+    val ctxt' = map_naming (K naming') ctxt;
+  in (scope, ctxt') end;
+
+val private = map_naming o Name_Space.private;
+val concealed = map_naming Name_Space.concealed;
+
 
 (* name spaces *)
 
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -47,7 +47,7 @@
                     |> filter completed
                     |> map (fn a => (a, ("system_option", a))));
               val report = Markup.markup_report (Completion.reported_text completion);
-            in cat_error msg report end;
+            in error (msg ^ report) end;
         val _ = Context_Position.report ctxt pos markup;
       in ML_Syntax.print_string name end)) #>
 
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Pure/PIDE/batch_session.scala
--- a/src/Pure/PIDE/batch_session.scala	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/PIDE/batch_session.scala	Wed Apr 01 22:40:41 2015 +0200
@@ -19,7 +19,7 @@
     session: String): Batch_Session =
   {
     val (_, session_tree) =
-      Build.find_sessions(options, dirs).selection(false, false, Nil, List(session))
+      Build.find_sessions(options, dirs).selection(sessions = List(session))
     val session_info = session_tree(session)
     val parent_session =
       session_info.parent getOrElse error("No parent session for " + quote(session))
@@ -29,7 +29,7 @@
         dirs = dirs, sessions = List(parent_session)) != 0)
       new RuntimeException
 
-    val deps = Build.dependencies(Build.Ignore_Progress, false, verbose, false, session_tree)
+    val deps = Build.dependencies(verbose = verbose, tree = session_tree)
     val resources =
     {
       val content = deps(parent_session)
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/Pure.thy	Wed Apr 01 22:40:41 2015 +0200
@@ -33,7 +33,7 @@
   and "bundle" :: thy_decl
   and "include" "including" :: prf_decl
   and "print_bundles" :: diag
-  and "context" "locale" :: thy_decl_block
+  and "context" "locale" "experiment" :: thy_decl_block
   and "sublocale" "interpretation" :: thy_goal
   and "interpret" :: prf_goal % "proof"
   and "class" :: thy_decl_block
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Pure/ROOT
--- a/src/Pure/ROOT	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/ROOT	Wed Apr 01 22:40:41 2015 +0200
@@ -121,6 +121,7 @@
     "Isar/code.ML"
     "Isar/context_rules.ML"
     "Isar/element.ML"
+    "Isar/experiment.ML"
     "Isar/expression.ML"
     "Isar/generic_target.ML"
     "Isar/isar_cmd.ML"
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/ROOT.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -273,6 +273,7 @@
 use "Isar/expression.ML";
 use "Isar/class_declaration.ML";
 use "Isar/bundle.ML";
+use "Isar/experiment.ML";
 
 use "simplifier.ML";
 use "Tools/plugin.ML";
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/Tools/build.scala	Wed Apr 01 22:40:41 2015 +0200
@@ -162,12 +162,18 @@
     def apply(name: String): Session_Info = graph.get_node(name)
     def isDefinedAt(name: String): Boolean = graph.defined(name)
 
-    def selection(requirements: Boolean, all_sessions: Boolean,
-      session_groups: List[String], sessions: List[String]): (List[String], Session_Tree) =
+    def selection(
+      requirements: Boolean = false,
+      all_sessions: Boolean = false,
+      session_groups: List[String] = Nil,
+      exclude_sessions: List[String] = Nil,
+      sessions: List[String] = Nil): (List[String], Session_Tree) =
     {
-      val bad_sessions = sessions.filterNot(isDefinedAt(_))
+      val bad_sessions =
+        SortedSet((exclude_sessions ::: sessions).filterNot(isDefinedAt(_)): _*).toList
       if (bad_sessions.nonEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
 
+      val excluded = graph.all_succs(exclude_sessions).toSet
       val pre_selected =
       {
         if (all_sessions) graph.keys
@@ -179,7 +185,8 @@
             if info.select || select(name) || apply(name).groups.exists(select_group)
           } yield name).toList
         }
-      }
+      }.filterNot(excluded)
+
       val selected =
         if (requirements) (graph.all_preds(pre_selected).toSet -- pre_selected).toList
         else pre_selected
@@ -427,8 +434,13 @@
     def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
   }
 
-  def dependencies(progress: Progress, inlined_files: Boolean,
-      verbose: Boolean, list_files: Boolean, tree: Session_Tree): Deps =
+  def dependencies(
+      progress: Progress = Ignore_Progress,
+      inlined_files: Boolean = false,
+      verbose: Boolean = false,
+      list_files: Boolean = false,
+      check_keywords: Set[String] = Set.empty,
+      tree: Session_Tree): Deps =
     Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
       { case (deps, (name, info)) =>
           if (progress.stopped) throw Exn.Interrupt()
@@ -484,16 +496,20 @@
             val keywords = thy_deps.keywords
             val syntax = thy_deps.syntax.asInstanceOf[Outer_Syntax]
 
+            val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
             val loaded_files = if (inlined_files) thy_deps.loaded_files else Nil
 
             val all_files =
-              (thy_deps.deps.map(dep => Path.explode(dep.name.node)) ::: loaded_files :::
+              (theory_files ::: loaded_files :::
                 info.files.map(file => info.dir + file) :::
                 info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
 
             if (list_files)
               progress.echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
 
+            if (check_keywords.nonEmpty)
+              Check_Keywords.check_keywords(progress, syntax.keywords, check_keywords, theory_files)
+
             val sources = all_files.map(p => (p, SHA1.digest(p.file)))
 
             val session_graph = thy_deps.deps_graph(info.parent getOrElse "", loaded_theories0)
@@ -516,8 +532,8 @@
     dirs: List[Path],
     sessions: List[String]): Deps =
   {
-    val (_, tree) = find_sessions(options, dirs = dirs).selection(false, false, Nil, sessions)
-    dependencies(Ignore_Progress, inlined_files, false, false, tree)
+    val (_, tree) = find_sessions(options, dirs = dirs).selection(sessions = sessions)
+    dependencies(inlined_files = inlined_files, tree = tree)
   }
 
   def session_content(
@@ -737,18 +753,20 @@
     session_groups: List[String] = Nil,
     max_jobs: Int = 1,
     list_files: Boolean = false,
+    check_keywords: Set[String] = Set.empty,
     no_build: Boolean = false,
     system_mode: Boolean = false,
     verbose: Boolean = false,
+    exclude_sessions: List[String] = Nil,
     sessions: List[String] = Nil): Map[String, Int] =
   {
     /* session tree and dependencies */
 
     val full_tree = find_sessions(options.int("completion_limit") = 0, dirs, select_dirs)
     val (selected, selected_tree) =
-      full_tree.selection(requirements, all_sessions, session_groups, sessions)
+      full_tree.selection(requirements, all_sessions, session_groups, exclude_sessions, sessions)
 
-    val deps = dependencies(progress, true, verbose, list_files, selected_tree)
+    val deps = dependencies(progress, true, verbose, list_files, check_keywords, selected_tree)
 
     def make_stamp(name: String): String =
       sources_stamp(selected_tree(name).entry_digest :: deps.sources(name))
@@ -988,15 +1006,17 @@
     session_groups: List[String] = Nil,
     max_jobs: Int = 1,
     list_files: Boolean = false,
+    check_keywords: Set[String] = Set.empty,
     no_build: Boolean = false,
     system_mode: Boolean = false,
     verbose: Boolean = false,
+    exclude_sessions: List[String] = Nil,
     sessions: List[String] = Nil): Int =
   {
     val results =
-      build_results(options, progress, requirements, all_sessions,
-        build_heap, clean_build, dirs, select_dirs, session_groups, max_jobs,
-        list_files, no_build, system_mode, verbose, sessions)
+      build_results(options, progress, requirements, all_sessions, build_heap, clean_build,
+        dirs, select_dirs, session_groups, max_jobs, list_files, check_keywords,
+        no_build, system_mode, verbose, exclude_sessions, sessions)
 
     val rc = (0 /: results)({ case (rc1, (_, rc2)) => rc1 max rc2 })
     if (rc != 0 && (verbose || !no_build)) {
@@ -1024,13 +1044,15 @@
           Properties.Value.Boolean(no_build) ::
           Properties.Value.Boolean(system_mode) ::
           Properties.Value.Boolean(verbose) ::
-          Command_Line.Chunks(dirs, select_dirs, session_groups, build_options, sessions) =>
+          Command_Line.Chunks(dirs, select_dirs, session_groups, check_keywords,
+              build_options, exclude_sessions, sessions) =>
             val options = (Options.init() /: build_options)(_ + _)
             val progress = new Console_Progress(verbose)
             progress.interrupt_handler {
               build(options, progress, requirements, all_sessions, build_heap, clean_build,
                 dirs.map(Path.explode(_)), select_dirs.map(Path.explode(_)), session_groups,
-                max_jobs, list_files, no_build, system_mode, verbose, sessions)
+                max_jobs, list_files, check_keywords.toSet, no_build, system_mode,
+                verbose, exclude_sessions, sessions)
             }
         case _ => error("Bad arguments:\n" + cat_lines(args))
       }
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Pure/Tools/check_keywords.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/check_keywords.scala	Wed Apr 01 22:40:41 2015 +0200
@@ -0,0 +1,54 @@
+/*  Title:      Pure/Tools/check_keywords.scala
+    Author:     Makarius
+
+Check theory sources for conflicts with proposed keywords.
+*/
+
+package isabelle
+
+
+object Check_Keywords
+{
+  def conflicts(
+    keywords: Keyword.Keywords,
+    check: Set[String],
+    input: CharSequence,
+    start: Token.Pos): List[(Token, Position.T)] =
+  {
+    object Parser extends Parse.Parser
+    {
+      private val conflict =
+        position(token("token", tok => !(tok.is_command || tok.is_keyword) && check(tok.source)))
+      private val other = token("token", _ => true)
+      private val item = conflict ^^ (x => Some(x)) | other ^^ (_ => None)
+
+      val result =
+        parse_all(rep(item), Token.reader(Token.explode(keywords, input), start)) match {
+          case Success(res, _) => for (Some(x) <- res) yield x
+          case bad => error(bad.toString)
+        }
+    }
+    Parser.result
+  }
+
+  def check_keywords(
+    progress: Build.Progress,
+    keywords: Keyword.Keywords,
+    check: Set[String],
+    paths: List[Path])
+  {
+    val parallel_args = paths.map(path => (File.read(path), Token.Pos.file(path.expand.implode)))
+
+    val bad =
+      Par_List.map((arg: (String, Token.Pos)) => {
+        if (progress.stopped) throw Exn.Interrupt()
+        conflicts(keywords, check, arg._1, arg._2)
+      }, parallel_args).flatten
+
+    for ((tok, pos) <- bad) {
+      progress.echo(Output.warning_text(
+        "keyword conflict: " + tok.kind.toString + " " + quote(tok.content) +
+          Position.here(pos)))
+    }
+  }
+}
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -328,7 +328,7 @@
 local
 
 val index_ord = option_ord (K EQUAL);
-val hidden_ord = bool_ord o apply2 Long_Name.is_hidden;
+val hidden_ord = bool_ord o apply2 (is_some o Long_Name.dest_hidden);
 val qual_ord = int_ord o apply2 Long_Name.qualification;
 val txt_ord = int_ord o apply2 size;
 
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Pure/Tools/named_theorems.ML
--- a/src/Pure/Tools/named_theorems.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/Tools/named_theorems.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -61,7 +61,7 @@
 
 fun declare binding descr lthy =
   let
-    val name = Name_Space.full_name (Local_Theory.naming_of lthy) binding;
+    val name = Local_Theory.full_name lthy binding;
     val description =
       "declaration of " ^ (if descr = "" then Binding.name_of binding ^ " rules" else descr);
     val lthy' = lthy
@@ -86,7 +86,7 @@
       let
         val thy = Proof_Context.theory_of ctxt;
         val name = Global_Theory.check_fact thy (xname, pos);
-        val _ = get ctxt name handle ERROR msg => cat_error msg (Position.here pos);
+        val _ = get ctxt name handle ERROR msg => error (msg ^ Position.here pos);
       in ML_Syntax.print_string name end)));
 
 end;
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Pure/Tools/plugin.ML
--- a/src/Pure/Tools/plugin.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/Tools/plugin.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -138,9 +138,9 @@
 
 fun apply change_naming (interp: interp) (data: data) lthy =
   lthy
-  |> change_naming ? Local_Theory.map_naming (K (#naming data))
+  |> change_naming ? Local_Theory.map_background_naming (K (#naming data))
   |> #apply interp (#value data)
-  |> Local_Theory.restore_naming lthy;
+  |> Local_Theory.restore_background_naming lthy;
 
 fun unfinished data (interp: interp, data') =
   (interp,
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Pure/build-jars
--- a/src/Pure/build-jars	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/build-jars	Wed Apr 01 22:40:41 2015 +0200
@@ -92,6 +92,7 @@
   Tools/build.scala
   Tools/build_console.scala
   Tools/build_doc.scala
+  Tools/check_keywords.scala
   Tools/check_source.scala
   Tools/doc.scala
   Tools/main.scala
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/facts.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -166,13 +166,13 @@
 
 (* retrieve *)
 
-val defined = is_some oo (Name_Space.lookup_key o facts_of);
+val defined = Name_Space.defined o facts_of;
 
 fun lookup context facts name =
-  (case Name_Space.lookup_key (facts_of facts) name of
+  (case Name_Space.lookup (facts_of facts) name of
     NONE => NONE
-  | SOME (_, Static ths) => SOME (true, ths)
-  | SOME (_, Dynamic f) => SOME (false, f context));
+  | SOME (Static ths) => SOME (true, ths)
+  | SOME (Dynamic f) => SOME (false, f context));
 
 fun retrieve context facts (xname, pos) =
   let
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/sign.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -101,6 +101,8 @@
     (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory
   val add_trrules: Ast.ast Syntax.trrule list -> theory -> theory
   val del_trrules: Ast.ast Syntax.trrule list -> theory -> theory
+  val get_scope: theory -> Binding.scope option
+  val new_scope: theory -> Binding.scope * theory
   val new_group: theory -> theory
   val reset_group: theory -> theory
   val add_path: string -> theory -> theory
@@ -109,6 +111,8 @@
   val mandatory_path: string -> theory -> theory
   val qualified_path: bool -> binding -> theory -> theory
   val local_path: theory -> theory
+  val private: Binding.scope -> theory -> theory
+  val concealed: theory -> theory
   val hide_class: bool -> string -> theory -> theory
   val hide_type: bool -> string -> theory -> theory
   val hide_const: bool -> string -> theory -> theory
@@ -499,6 +503,14 @@
 
 (* naming *)
 
+val get_scope = Name_Space.get_scope o naming_of;
+
+fun new_scope thy =
+  let
+    val (scope, naming') = Name_Space.new_scope (naming_of thy);
+    val thy' = map_naming (K naming') thy;
+  in (scope, thy') end;
+
 val new_group = map_naming Name_Space.new_group;
 val reset_group = map_naming Name_Space.reset_group;
 
@@ -510,6 +522,9 @@
 
 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
 
+val private = map_naming o Name_Space.private;
+val concealed = map_naming Name_Space.concealed;
+
 
 (* hide names *)
 
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/thm.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -590,8 +590,8 @@
 fun axiom theory name =
   let
     fun get_ax thy =
-      Name_Space.lookup_key (Theory.axiom_table thy) name
-      |> Option.map (fn (_, prop) =>
+      Name_Space.lookup (Theory.axiom_table thy) name
+      |> Option.map (fn prop =>
            let
              val der = deriv_rule0 (Proofterm.axm_proof name prop);
              val maxidx = maxidx_of_term prop;
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Pure/type.ML
--- a/src/Pure/type.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/type.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -254,7 +254,7 @@
 
 fun undecl_type c = "Undeclared type constructor: " ^ quote c;
 
-fun lookup_type (TSig {types, ...}) = Option.map #2 o Name_Space.lookup_key types;
+fun lookup_type (TSig {types, ...}) = Name_Space.lookup types;
 
 fun check_decl context (TSig {types, ...}) (c, pos) =
   Name_Space.check_reports context types (c, [pos]);
@@ -659,8 +659,9 @@
   let
     val types' = f types;
     val _ =
+      not (Name_Space.defined types' "dummy") orelse
       Name_Space.intern (Name_Space.space_of_table types') "dummy" = "dummy" orelse
-        error "Illegal declaration of dummy type";
+      error "Illegal declaration of dummy type";
   in (classes, default, types') end);
 
 fun syntactic tsig (Type (c, Ts)) =
diff -r 2d929c178283 -r 9d70a39d1cf3 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Wed Apr 01 19:17:41 2015 +0200
+++ b/src/Pure/variable.ML	Wed Apr 01 22:40:41 2015 +0200
@@ -340,14 +340,14 @@
 fun restore_proper_fixes ctxt = Config.put proper_fixes (Config.get ctxt proper_fixes);
 
 fun is_improper ctxt x =
-  (case Name_Space.lookup_key (fixes_of ctxt) x of
-    SOME (_, (_, proper)) => not proper
+  (case Name_Space.lookup (fixes_of ctxt) x of
+    SOME (_, proper) => not proper
   | NONE => false);
 
 
 (* specialized name space *)
 
-val is_fixed = Name_Space.defined_entry o fixes_space;
+val is_fixed = Name_Space.defined o fixes_of;
 fun is_newly_fixed inner outer = is_fixed inner andf (not o is_fixed outer);
 
 val fixed_ord = Name_Space.entry_ord o fixes_space;
@@ -358,8 +358,8 @@
   in if is_fixed ctxt x' then SOME x' else NONE end;
 
 fun revert_fixed ctxt x =
-  (case Name_Space.lookup_key (fixes_of ctxt) x of
-    SOME (_, (x', _)) => if intern_fixed ctxt x' = x then x' else x
+  (case Name_Space.lookup (fixes_of ctxt) x of
+    SOME (x', _) => if intern_fixed ctxt x' = x then x' else x
   | NONE => x);
 
 fun markup_fixed ctxt x =