src/Pure/Isar/locale.ML

 
 fun pretty_reg ctxt export (name, morph) =
   let
     val thy = Proof_Context.theory_of ctxt;
     val morph' = morph $> export;
-    fun print_qual (qual, mandatory) = qual ^ (if mandatory then "!" else "?");
+    fun print_qual (qual, mandatory) = qual ^ (if mandatory then "" else "?");
     fun prt_quals qs = Pretty.str (space_implode "." (map print_qual qs));
     val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
     fun prt_term' t =
       if Config.get ctxt show_types
       then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::",