uniform mandatory qualifier for all locale expressions, including 'statespace' parent;
removed obsolete '!' syntax;

--- a/NEWS	Mon Nov 09 15:48:17 2015 +0100
+++ b/NEWS	Mon Nov 09 21:04:49 2015 +0100
@@ -276,12 +276,13 @@
 
 *** Pure ***
 
-* Qualifiers in locale expressions default to mandatory ('!')
-regardless of the command.  Previously, for 'locale' and 'sublocale'
-the default was optional ('?').  INCOMPATIBILITY
+* Qualifiers in locale expressions default to mandatory ('!') regardless
+of the command. Previously, for 'locale' and 'sublocale' the default was
+optional ('?'). The old synatx '!' has been discontinued.
+INCOMPATIBILITY, remove '!' and add '?' as required.
 
 * Keyword 'rewrites' identifies rewrite morphisms in interpretation
-commands.  Previously, the keyword was 'where'.  INCOMPATIBILITY
+commands.  Previously, the keyword was 'where'.  INCOMPATIBILITY.
 
 * Command 'print_definitions' prints dependencies of definitional
 specifications. This functionality used to be part of 'print_theory'.
@@ -501,7 +502,12 @@
 
 * Imperative_HOL: obsolete theory Legacy_Mrec has been removed.
 
-* Library/Omega_Words_Fun: Infinite words modeled as functions nat => 'a.
+* Library/Omega_Words_Fun: Infinite words modeled as functions nat =>
+'a.
+
+* HOL-Statespace: command 'statespace' uses mandatory qualifier for
+import of parent, as for general 'locale' expressions. INCOMPATIBILITY,
+remove '!' and add '?' as required.
 
 
 *** ML ***

--- a/src/Doc/Isar_Ref/Spec.thy	Mon Nov 09 15:48:17 2015 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy	Mon Nov 09 21:04:49 2015 +0100
@@ -462,44 +462,41 @@
 subsection \<open>Locale expressions \label{sec:locale-expr}\<close>
 
 text \<open>
-  A \<^emph>\<open>locale expression\<close> denotes a context composed of instances
-  of existing locales.  The context consists of the declaration
-  elements from the locale instances.  Redundant locale instances are
-  omitted according to roundup.
+  A \<^emph>\<open>locale expression\<close> denotes a context composed of instances of existing
+  locales. The context consists of the declaration elements from the locale
+  instances. Redundant locale instances are omitted according to roundup.
 
   @{rail \<open>
     @{syntax_def locale_expr}: (instance + '+') @{syntax for_fixes}
     ;
     instance: (qualifier ':')? @{syntax nameref} (pos_insts | named_insts)
     ;
-    qualifier: @{syntax name} ('?' | '!')?
+    qualifier: @{syntax name} ('?')?
     ;
     pos_insts: ('_' | @{syntax term})*
     ;
     named_insts: @'where' (@{syntax name} '=' @{syntax term} + @'and')
   \<close>}
 
-  A locale instance consists of a reference to a locale and either
-  positional or named parameter instantiations.  Identical
-  instantiations (that is, those that instantiate a parameter by itself)
-  may be omitted.  The notation `\<open>_\<close>' enables to omit the
-  instantiation for a parameter inside a positional instantiation.
+  A locale instance consists of a reference to a locale and either positional
+  or named parameter instantiations. Identical instantiations (that is, those
+  that instantiate a parameter by itself) may be omitted. The notation ``\<open>_\<close>''
+  enables to omit the instantiation for a parameter inside a positional
+  instantiation.
 
-  Terms in instantiations are from the context the locale expressions
-  is declared in.  Local names may be added to this context with the
-  optional @{keyword "for"} clause.  This is useful for shadowing names
-  bound in outer contexts, and for declaring syntax.  In addition,
-  syntax declarations from one instance are effective when parsing
-  subsequent instances of the same expression.
+  Terms in instantiations are from the context the locale expressions is
+  declared in. Local names may be added to this context with the optional
+  @{keyword "for"} clause. This is useful for shadowing names bound in outer
+  contexts, and for declaring syntax. In addition, syntax declarations from
+  one instance are effective when parsing subsequent instances of the same
+  expression.
 
-  Instances have an optional qualifier which applies to names in
-  declarations.  Names include local definitions and theorem names.
-  If present, the qualifier itself is either optional
-  (``\<^verbatim>\<open>?\<close>''), which means that it may be omitted on input of the
-  qualified name, or mandatory (``\<^verbatim>\<open>!\<close>'').  If neither
-  ``\<^verbatim>\<open>?\<close>'' nor ``\<^verbatim>\<open>!\<close>'' are present the default
-  is used, which is ``mandatory''.  Qualifiers play no role
-  in determining whether one locale instance subsumes another.
+  Instances have an optional qualifier which applies to names in declarations.
+  Names include local definitions and theorem names. If present, the qualifier
+  itself is either mandatory (default) or non-mandatory (when followed by
+  ``\<^verbatim>\<open>?\<close>''). Non-mandatory means that the qualifier may be omitted on input.
+  Qualifiers only affect name spaces; they play no role in determining whether
+  one locale instance subsumes another.
 \<close>
 
 

--- a/src/HOL/Statespace/state_space.ML	Mon Nov 09 15:48:17 2015 +0100
+++ b/src/HOL/Statespace/state_space.ML	Mon Nov 09 21:04:49 2015 +0100
@@ -642,7 +642,7 @@
 val renames = Scan.optional (@{keyword "["} |-- Parse.!!! (Parse.list1 rename --| @{keyword "]"})) [];
 
 val parent =
-  Parse_Spec.locale_prefix false --
+  Parse_Spec.locale_prefix --
   ((type_insts -- Parse.xname) || (Parse.xname >> pair [])) -- renames
     >> (fn ((prefix, (insts, name)), renames) => (prefix, (insts, name, renames)));
 

--- a/src/Pure/Isar/isar_syn.ML	Mon Nov 09 15:48:17 2015 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Mon Nov 09 21:04:49 2015 +0100
@@ -384,7 +384,7 @@
 (* locales *)
 
 val locale_val =
-  Parse_Spec.locale_expression true --
+  Parse_Spec.locale_expression --
     Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
   Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
 
@@ -403,7 +403,7 @@
           Toplevel.begin_local_theory true (Experiment.experiment_cmd elems #> snd)));
 
 val interpretation_args =
-  Parse.!!! (Parse_Spec.locale_expression true) --
+  Parse.!!! Parse_Spec.locale_expression --
     Scan.optional
       (@{keyword "rewrites"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
 
@@ -817,7 +817,7 @@
 val _ =
   Outer_Syntax.command @{command_keyword print_dependencies}
     "print dependencies of locale expression"
-    (Parse.opt_bang -- Parse_Spec.locale_expression true >> (fn (b, expr) =>
+    (Parse.opt_bang -- Parse_Spec.locale_expression >> (fn (b, expr) =>
       Toplevel.keep (fn state => Expression.print_dependencies (Toplevel.context_of state) b expr)));
 
 val _ =

--- a/src/Pure/Isar/parse_spec.ML	Mon Nov 09 15:48:17 2015 +0100
+++ b/src/Pure/Isar/parse_spec.ML	Mon Nov 09 21:04:49 2015 +0100
@@ -19,9 +19,9 @@
   val locale_fixes: (binding * string option * mixfix) list parser
   val locale_insts: (string option list * (Attrib.binding * string) list) parser
   val class_expression: string list parser
-  val locale_prefix: bool -> (string * bool) parser
+  val locale_prefix: (string * bool) parser
   val locale_keyword: string parser
-  val locale_expression: bool -> Expression.expression parser
+  val locale_expression: Expression.expression parser
   val context_element: Element.context parser
   val statement: (Attrib.binding * (string * string list) list) list parser
   val if_statement: (Attrib.binding * (string * string list) list) list parser
@@ -105,11 +105,9 @@
 
 in
 
-fun locale_prefix mandatory =
+val locale_prefix =
   Scan.optional
-    (Parse.name --
-      (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --|
-      Parse.$$$ ":")
+    (Parse.name -- (Scan.option (Parse.$$$ "?") >> is_none) --| Parse.$$$ ":")
     ("", false);
 
 val locale_keyword =
@@ -118,10 +116,11 @@
 
 val class_expression = plus1_unless locale_keyword Parse.class;
 
-fun locale_expression mandatory =
+val locale_expression =
   let
     val expr2 = Parse.position Parse.xname;
-    val expr1 = locale_prefix mandatory -- expr2 --
+    val expr1 =
+      locale_prefix -- expr2 --
       Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
     val expr0 = plus1_unless locale_keyword expr1;
   in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;

--- a/src/Tools/permanent_interpretation.ML	Mon Nov 09 15:48:17 2015 +0100
+++ b/src/Tools/permanent_interpretation.ML	Mon Nov 09 21:04:49 2015 +0100
@@ -99,7 +99,7 @@
 val _ =
   Outer_Syntax.local_theory_to_proof @{command_keyword permanent_interpretation}
     "prove interpretation of locale expression into named theory"
-    (Parse.!!! (Parse_Spec.locale_expression true) --
+    (Parse.!!! Parse_Spec.locale_expression --
       Scan.optional (@{keyword "defining"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
         -- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "="} -- Parse.term))) [] --
       Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []