more conventional naming scheme: names_long, names_short, names_unique;
authorwenzelm
Tue May 03 22:27:32 2011 +0200 (2011-05-03)
changeset 4266904dfffda5671
parent 42668 b98f22593f97
child 42672 d34154b08579
more conventional naming scheme: names_long, names_short, names_unique;
NEWS
doc-src/Codegen/Thy/Setup.thy
doc-src/IsarRef/Thy/Document_Preparation.thy
doc-src/IsarRef/Thy/Inner_Syntax.thy
doc-src/IsarRef/Thy/document/Document_Preparation.tex
doc-src/IsarRef/Thy/document/Inner_Syntax.tex
doc-src/LaTeXsugar/Sugar/Sugar.thy
doc-src/LaTeXsugar/Sugar/document/Sugar.tex
doc-src/TutorialI/Misc/Itrev.thy
src/Pure/General/name_space.ML
src/Pure/Isar/attrib.ML
src/Pure/ProofGeneral/preferences.ML
src/Pure/Thy/thy_output.ML
src/Pure/Tools/find_theorems.ML
     1.1 --- a/NEWS	Tue May 03 22:26:16 2011 +0200
     1.2 +++ b/NEWS	Tue May 03 22:27:32 2011 +0200
     1.3 @@ -37,12 +37,16 @@
     1.4  Note that automated detection from the file-system or search path has
     1.5  been discontinued.  INCOMPATIBILITY.
     1.6  
     1.7 -* Name space: proper configuration options "long_names",
     1.8 -"short_names", "unique_names" instead of former unsynchronized
     1.9 -references.  Minor INCOMPATIBILITY, need to declare options in context
    1.10 -like this:
    1.11 -
    1.12 -  declare [[unique_names = false]]
    1.13 +* Name space: former unsynchronized references are now proper
    1.14 +configuration options, with more conventional names:
    1.15 +
    1.16 +  long_names   ~> names_long
    1.17 +  short_names  ~> names_short
    1.18 +  unique_names ~> names_unique
    1.19 +
    1.20 +Minor INCOMPATIBILITY, need to declare options in context like this:
    1.21 +
    1.22 +  declare [[names_unique = false]]
    1.23  
    1.24  * Literal facts `prop` may contain dummy patterns, e.g. `_ = _`.  Note
    1.25  that the result needs to be unique, which means fact specifications
     2.1 --- a/doc-src/Codegen/Thy/Setup.thy	Tue May 03 22:26:16 2011 +0200
     2.2 +++ b/doc-src/Codegen/Thy/Setup.thy	Tue May 03 22:27:32 2011 +0200
     2.3 @@ -22,6 +22,6 @@
     2.4  
     2.5  setup {* Code_Target.set_default_code_width 74 *}
     2.6  
     2.7 -declare [[unique_names = false]]
     2.8 +declare [[names_unique = false]]
     2.9  
    2.10  end
     3.1 --- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Tue May 03 22:26:16 2011 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Tue May 03 22:27:32 2011 +0200
     3.3 @@ -341,16 +341,16 @@
     3.4    \item @{antiquotation_option_def show_abbrevs}~@{text "= bool"}
     3.5    controls folding of abbreviations.
     3.6  
     3.7 -  \item @{antiquotation_option_def long_names}~@{text "= bool"} forces
     3.8 +  \item @{antiquotation_option_def names_long}~@{text "= bool"} forces
     3.9    names of types and constants etc.\ to be printed in their fully
    3.10    qualified internal form.
    3.11  
    3.12 -  \item @{antiquotation_option_def short_names}~@{text "= bool"}
    3.13 +  \item @{antiquotation_option_def names_short}~@{text "= bool"}
    3.14    forces names of types and constants etc.\ to be printed unqualified.
    3.15    Note that internalizing the output again in the current context may
    3.16    well yield a different result.
    3.17  
    3.18 -  \item @{antiquotation_option_def unique_names}~@{text "= bool"}
    3.19 +  \item @{antiquotation_option_def names_unique}~@{text "= bool"}
    3.20    determines whether the printed version of qualified names should be
    3.21    made sufficiently long to avoid overlap with names declared further
    3.22    back.  Set to @{text false} for more concise output.
     4.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Tue May 03 22:26:16 2011 +0200
     4.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Tue May 03 22:27:32 2011 +0200
     4.3 @@ -100,9 +100,9 @@
     4.4      @{attribute_def show_consts} & : & @{text attribute} & default @{text false} \\
     4.5      @{attribute_def show_abbrevs} & : & @{text attribute} & default @{text true} \\
     4.6      @{attribute_def show_brackets} & : & @{text attribute} & default @{text false} \\
     4.7 -    @{attribute_def long_names} & : & @{text attribute} & default @{text false} \\
     4.8 -    @{attribute_def short_names} & : & @{text attribute} & default @{text false} \\
     4.9 -    @{attribute_def unique_names} & : & @{text attribute} & default @{text true} \\
    4.10 +    @{attribute_def names_long} & : & @{text attribute} & default @{text false} \\
    4.11 +    @{attribute_def names_short} & : & @{text attribute} & default @{text false} \\
    4.12 +    @{attribute_def names_unique} & : & @{text attribute} & default @{text true} \\
    4.13      @{attribute_def eta_contract} & : & @{text attribute} & default @{text true} \\
    4.14      @{attribute_def goals_limit} & : & @{text attribute} & default @{text 10} \\
    4.15      @{attribute_def show_main_goal} & : & @{text attribute} & default @{text false} \\
    4.16 @@ -144,8 +144,8 @@
    4.17    pretty printed entities may occasionally help to diagnose problems
    4.18    with operator priorities, for example.
    4.19  
    4.20 -  \item @{attribute long_names}, @{attribute short_names}, and
    4.21 -  @{attribute unique_names} control the way of printing fully
    4.22 +  \item @{attribute names_long}, @{attribute names_short}, and
    4.23 +  @{attribute names_unique} control the way of printing fully
    4.24    qualified internal names in external form.  See also
    4.25    \secref{sec:antiq} for the document antiquotation options of the
    4.26    same names.
     5.1 --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Tue May 03 22:26:16 2011 +0200
     5.2 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Tue May 03 22:27:32 2011 +0200
     5.3 @@ -497,16 +497,16 @@
     5.4    \item \indexdef{}{antiquotation option}{show\_abbrevs}\hypertarget{antiquotation option.show-abbrevs}{\hyperlink{antiquotation option.show-abbrevs}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}abbrevs}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}}
     5.5    controls folding of abbreviations.
     5.6  
     5.7 -  \item \indexdef{}{antiquotation option}{long\_names}\hypertarget{antiquotation option.long-names}{\hyperlink{antiquotation option.long-names}{\mbox{\isa{long{\isaliteral{5F}{\isacharunderscore}}names}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} forces
     5.8 +  \item \indexdef{}{antiquotation option}{names\_long}\hypertarget{antiquotation option.names-long}{\hyperlink{antiquotation option.names-long}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}long}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}} forces
     5.9    names of types and constants etc.\ to be printed in their fully
    5.10    qualified internal form.
    5.11  
    5.12 -  \item \indexdef{}{antiquotation option}{short\_names}\hypertarget{antiquotation option.short-names}{\hyperlink{antiquotation option.short-names}{\mbox{\isa{short{\isaliteral{5F}{\isacharunderscore}}names}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}}
    5.13 +  \item \indexdef{}{antiquotation option}{names\_short}\hypertarget{antiquotation option.names-short}{\hyperlink{antiquotation option.names-short}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}short}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}}
    5.14    forces names of types and constants etc.\ to be printed unqualified.
    5.15    Note that internalizing the output again in the current context may
    5.16    well yield a different result.
    5.17  
    5.18 -  \item \indexdef{}{antiquotation option}{unique\_names}\hypertarget{antiquotation option.unique-names}{\hyperlink{antiquotation option.unique-names}{\mbox{\isa{unique{\isaliteral{5F}{\isacharunderscore}}names}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}}
    5.19 +  \item \indexdef{}{antiquotation option}{names\_unique}\hypertarget{antiquotation option.names-unique}{\hyperlink{antiquotation option.names-unique}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}unique}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}}
    5.20    determines whether the printed version of qualified names should be
    5.21    made sufficiently long to avoid overlap with names declared further
    5.22    back.  Set to \isa{false} for more concise output.
     6.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Tue May 03 22:26:16 2011 +0200
     6.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Tue May 03 22:27:32 2011 +0200
     6.3 @@ -175,9 +175,9 @@
     6.4      \indexdef{}{attribute}{show\_consts}\hypertarget{attribute.show-consts}{\hyperlink{attribute.show-consts}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}consts}}}} & : & \isa{attribute} & default \isa{false} \\
     6.5      \indexdef{}{attribute}{show\_abbrevs}\hypertarget{attribute.show-abbrevs}{\hyperlink{attribute.show-abbrevs}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}abbrevs}}}} & : & \isa{attribute} & default \isa{true} \\
     6.6      \indexdef{}{attribute}{show\_brackets}\hypertarget{attribute.show-brackets}{\hyperlink{attribute.show-brackets}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}brackets}}}} & : & \isa{attribute} & default \isa{false} \\
     6.7 -    \indexdef{}{attribute}{long\_names}\hypertarget{attribute.long-names}{\hyperlink{attribute.long-names}{\mbox{\isa{long{\isaliteral{5F}{\isacharunderscore}}names}}}} & : & \isa{attribute} & default \isa{false} \\
     6.8 -    \indexdef{}{attribute}{short\_names}\hypertarget{attribute.short-names}{\hyperlink{attribute.short-names}{\mbox{\isa{short{\isaliteral{5F}{\isacharunderscore}}names}}}} & : & \isa{attribute} & default \isa{false} \\
     6.9 -    \indexdef{}{attribute}{unique\_names}\hypertarget{attribute.unique-names}{\hyperlink{attribute.unique-names}{\mbox{\isa{unique{\isaliteral{5F}{\isacharunderscore}}names}}}} & : & \isa{attribute} & default \isa{true} \\
    6.10 +    \indexdef{}{attribute}{names\_long}\hypertarget{attribute.names-long}{\hyperlink{attribute.names-long}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}long}}}} & : & \isa{attribute} & default \isa{false} \\
    6.11 +    \indexdef{}{attribute}{names\_short}\hypertarget{attribute.names-short}{\hyperlink{attribute.names-short}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}short}}}} & : & \isa{attribute} & default \isa{false} \\
    6.12 +    \indexdef{}{attribute}{names\_unique}\hypertarget{attribute.names-unique}{\hyperlink{attribute.names-unique}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}unique}}}} & : & \isa{attribute} & default \isa{true} \\
    6.13      \indexdef{}{attribute}{eta\_contract}\hypertarget{attribute.eta-contract}{\hyperlink{attribute.eta-contract}{\mbox{\isa{eta{\isaliteral{5F}{\isacharunderscore}}contract}}}} & : & \isa{attribute} & default \isa{true} \\
    6.14      \indexdef{}{attribute}{goals\_limit}\hypertarget{attribute.goals-limit}{\hyperlink{attribute.goals-limit}{\mbox{\isa{goals{\isaliteral{5F}{\isacharunderscore}}limit}}}} & : & \isa{attribute} & default \isa{{\isadigit{1}}{\isadigit{0}}} \\
    6.15      \indexdef{}{attribute}{show\_main\_goal}\hypertarget{attribute.show-main-goal}{\hyperlink{attribute.show-main-goal}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}main{\isaliteral{5F}{\isacharunderscore}}goal}}}} & : & \isa{attribute} & default \isa{false} \\
    6.16 @@ -219,8 +219,8 @@
    6.17    pretty printed entities may occasionally help to diagnose problems
    6.18    with operator priorities, for example.
    6.19  
    6.20 -  \item \hyperlink{attribute.long-names}{\mbox{\isa{long{\isaliteral{5F}{\isacharunderscore}}names}}}, \hyperlink{attribute.short-names}{\mbox{\isa{short{\isaliteral{5F}{\isacharunderscore}}names}}}, and
    6.21 -  \hyperlink{attribute.unique-names}{\mbox{\isa{unique{\isaliteral{5F}{\isacharunderscore}}names}}} control the way of printing fully
    6.22 +  \item \hyperlink{attribute.names-long}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}long}}}, \hyperlink{attribute.names-short}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}short}}}, and
    6.23 +  \hyperlink{attribute.names-unique}{\mbox{\isa{names{\isaliteral{5F}{\isacharunderscore}}unique}}} control the way of printing fully
    6.24    qualified internal names in external form.  See also
    6.25    \secref{sec:antiq} for the document antiquotation options of the
    6.26    same names.
     7.1 --- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Tue May 03 22:26:16 2011 +0200
     7.2 +++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Tue May 03 22:27:32 2011 +0200
     7.3 @@ -152,7 +152,7 @@
     7.4  the qualified name, for example @{text "T.length"}, where @{text T} is the
     7.5  theory it is defined in, to distinguish it from the predefined @{const[source]
     7.6  "List.length"}. In case there is no danger of confusion, you can insist on
     7.7 -short names (no qualifiers) by setting the \verb!short_names!
     7.8 +short names (no qualifiers) by setting the \verb!names_short!
     7.9  configuration option in the context.
    7.10  *}
    7.11  
     8.1 --- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Tue May 03 22:26:16 2011 +0200
     8.2 +++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Tue May 03 22:27:32 2011 +0200
     8.3 @@ -195,7 +195,7 @@
     8.4  If there are multiple declarations of the same name, Isabelle prints
     8.5  the qualified name, for example \isa{T{\isaliteral{2E}{\isachardot}}length}, where \isa{T} is the
     8.6  theory it is defined in, to distinguish it from the predefined \isa{{\isaliteral{22}{\isachardoublequote}}List{\isaliteral{2E}{\isachardot}}length{\isaliteral{22}{\isachardoublequote}}}. In case there is no danger of confusion, you can insist on
     8.7 -short names (no qualifiers) by setting the \verb!short_names!
     8.8 +short names (no qualifiers) by setting the \verb!names_short!
     8.9  configuration option in the context.%
    8.10  \end{isamarkuptext}%
    8.11  \isamarkuptrue%
     9.1 --- a/doc-src/TutorialI/Misc/Itrev.thy	Tue May 03 22:26:16 2011 +0200
     9.2 +++ b/doc-src/TutorialI/Misc/Itrev.thy	Tue May 03 22:27:32 2011 +0200
     9.3 @@ -2,7 +2,7 @@
     9.4  theory Itrev
     9.5  imports Main
     9.6  begin
     9.7 -declare [[unique_names = false]]
     9.8 +declare [[names_unique = false]]
     9.9  (*>*)
    9.10  
    9.11  section{*Induction Heuristics*}
    9.12 @@ -141,6 +141,6 @@
    9.13  \index{induction heuristics|)}
    9.14  *}
    9.15  (*<*)
    9.16 -declare [[unique_names = true]]
    9.17 +declare [[names_unique = true]]
    9.18  end
    9.19  (*>*)
    10.1 --- a/src/Pure/General/name_space.ML	Tue May 03 22:26:16 2011 +0200
    10.2 +++ b/src/Pure/General/name_space.ML	Tue May 03 22:27:32 2011 +0200
    10.3 @@ -20,15 +20,15 @@
    10.4    val markup: T -> string -> Markup.T
    10.5    val is_concealed: T -> string -> bool
    10.6    val intern: T -> xstring -> string
    10.7 -  val long_names_default: bool Unsynchronized.ref
    10.8 -  val long_names_raw: Config.raw
    10.9 -  val long_names: bool Config.T
   10.10 -  val short_names_default: bool Unsynchronized.ref
   10.11 -  val short_names_raw: Config.raw
   10.12 -  val short_names: bool Config.T
   10.13 -  val unique_names_default: bool Unsynchronized.ref
   10.14 -  val unique_names_raw: Config.raw
   10.15 -  val unique_names: bool Config.T
   10.16 +  val names_long_default: bool Unsynchronized.ref
   10.17 +  val names_long_raw: Config.raw
   10.18 +  val names_long: bool Config.T
   10.19 +  val names_short_default: bool Unsynchronized.ref
   10.20 +  val names_short_raw: Config.raw
   10.21 +  val names_short: bool Config.T
   10.22 +  val names_unique_default: bool Unsynchronized.ref
   10.23 +  val names_unique_raw: Config.raw
   10.24 +  val names_unique: bool Config.T
   10.25    val extern: Proof.context -> T -> string -> xstring
   10.26    val hide: bool -> string -> T -> T
   10.27    val merge: T * T -> T
   10.28 @@ -161,33 +161,33 @@
   10.29  fun intern space xname = #1 (lookup space xname);
   10.30  
   10.31  
   10.32 -val long_names_default = Unsynchronized.ref false;
   10.33 -val long_names_raw = Config.declare "long_names" (fn _ => Config.Bool (! long_names_default));
   10.34 -val long_names = Config.bool long_names_raw;
   10.35 +val names_long_default = Unsynchronized.ref false;
   10.36 +val names_long_raw = Config.declare "names_long" (fn _ => Config.Bool (! names_long_default));
   10.37 +val names_long = Config.bool names_long_raw;
   10.38  
   10.39 -val short_names_default = Unsynchronized.ref false;
   10.40 -val short_names_raw = Config.declare "short_names" (fn _ => Config.Bool (! short_names_default));
   10.41 -val short_names = Config.bool short_names_raw;
   10.42 +val names_short_default = Unsynchronized.ref false;
   10.43 +val names_short_raw = Config.declare "names_short" (fn _ => Config.Bool (! names_short_default));
   10.44 +val names_short = Config.bool names_short_raw;
   10.45  
   10.46 -val unique_names_default = Unsynchronized.ref true;
   10.47 -val unique_names_raw = Config.declare "unique_names" (fn _ => Config.Bool (! unique_names_default));
   10.48 -val unique_names = Config.bool unique_names_raw;
   10.49 +val names_unique_default = Unsynchronized.ref true;
   10.50 +val names_unique_raw = Config.declare "names_unique" (fn _ => Config.Bool (! names_unique_default));
   10.51 +val names_unique = Config.bool names_unique_raw;
   10.52  
   10.53  fun extern ctxt space name =
   10.54    let
   10.55 -    val long_names = Config.get ctxt long_names;
   10.56 -    val short_names = Config.get ctxt short_names;
   10.57 -    val unique_names = Config.get ctxt unique_names;
   10.58 +    val names_long = Config.get ctxt names_long;
   10.59 +    val names_short = Config.get ctxt names_short;
   10.60 +    val names_unique = Config.get ctxt names_unique;
   10.61  
   10.62      fun valid require_unique xname =
   10.63        let val (name', is_unique) = lookup space xname
   10.64        in name = name' andalso (not require_unique orelse is_unique) end;
   10.65  
   10.66      fun ext [] = if valid false name then name else hidden name
   10.67 -      | ext (nm :: nms) = if valid unique_names nm then nm else ext nms;
   10.68 +      | ext (nm :: nms) = if valid names_unique nm then nm else ext nms;
   10.69    in
   10.70 -    if long_names then name
   10.71 -    else if short_names then Long_Name.base_name name
   10.72 +    if names_long then name
   10.73 +    else if names_short then Long_Name.base_name name
   10.74      else ext (get_accesses space name)
   10.75    end;
   10.76  
    11.1 --- a/src/Pure/Isar/attrib.ML	Tue May 03 22:26:16 2011 +0200
    11.2 +++ b/src/Pure/Isar/attrib.ML	Tue May 03 22:27:32 2011 +0200
    11.3 @@ -441,9 +441,9 @@
    11.4    register_config Printer.show_question_marks_raw #>
    11.5    register_config Syntax.ambiguity_level_raw #>
    11.6    register_config Syntax_Trans.eta_contract_raw #>
    11.7 -  register_config Name_Space.long_names_raw #>
    11.8 -  register_config Name_Space.short_names_raw #>
    11.9 -  register_config Name_Space.unique_names_raw #>
   11.10 +  register_config Name_Space.names_long_raw #>
   11.11 +  register_config Name_Space.names_short_raw #>
   11.12 +  register_config Name_Space.names_unique_raw #>
   11.13    register_config ML_Context.trace_raw #>
   11.14    register_config Proof_Context.show_abbrevs_raw #>
   11.15    register_config Goal_Display.goals_limit_raw #>
    12.1 --- a/src/Pure/ProofGeneral/preferences.ML	Tue May 03 22:26:16 2011 +0200
    12.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Tue May 03 22:27:32 2011 +0200
    12.3 @@ -124,7 +124,7 @@
    12.4    bool_pref Goal_Display.show_consts_default
    12.5      "show-consts"
    12.6      "Show types of consts in Isabelle goal display",
    12.7 -  bool_pref Name_Space.long_names_default
    12.8 +  bool_pref Name_Space.names_long_default
    12.9      "long-names"
   12.10      "Show fully qualified names in Isabelle terms",
   12.11    bool_pref Printer.show_brackets_default
    13.1 --- a/src/Pure/Thy/thy_output.ML	Tue May 03 22:26:16 2011 +0200
    13.2 +++ b/src/Pure/Thy/thy_output.ML	Tue May 03 22:27:32 2011 +0200
    13.3 @@ -450,9 +450,9 @@
    13.4  val _ = add_option "show_structs" (Config.put show_structs o boolean);
    13.5  val _ = add_option "show_question_marks" (Config.put show_question_marks o boolean);
    13.6  val _ = add_option "show_abbrevs" (Config.put show_abbrevs o boolean);
    13.7 -val _ = add_option "long_names" (Config.put Name_Space.long_names o boolean);
    13.8 -val _ = add_option "short_names" (Config.put Name_Space.short_names o boolean);
    13.9 -val _ = add_option "unique_names" (Config.put Name_Space.unique_names o boolean);
   13.10 +val _ = add_option "names_long" (Config.put Name_Space.names_long o boolean);
   13.11 +val _ = add_option "names_short" (Config.put Name_Space.names_short o boolean);
   13.12 +val _ = add_option "names_unique" (Config.put Name_Space.names_unique o boolean);
   13.13  val _ = add_option "eta_contract" (Config.put Syntax_Trans.eta_contract o boolean);
   13.14  val _ = add_option "display" (Config.put display o boolean);
   13.15  val _ = add_option "break" (Config.put break o boolean);
    14.1 --- a/src/Pure/Tools/find_theorems.ML	Tue May 03 22:26:16 2011 +0200
    14.2 +++ b/src/Pure/Tools/find_theorems.ML	Tue May 03 22:27:32 2011 +0200
    14.3 @@ -383,9 +383,9 @@
    14.4      val shorten =
    14.5        Name_Space.extern
    14.6          (ctxt
    14.7 -          |> Config.put Name_Space.long_names false
    14.8 -          |> Config.put Name_Space.short_names false
    14.9 -          |> Config.put Name_Space.unique_names false) space;
   14.10 +          |> Config.put Name_Space.names_long false
   14.11 +          |> Config.put Name_Space.names_short false
   14.12 +          |> Config.put Name_Space.names_unique false) space;
   14.13  
   14.14      fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
   14.15            nicer_name (shorten x, i) (shorten y, j)