merged;
authorwenzelm
Thu Dec 02 21:04:20 2010 +0100 (2010-12-02)
changeset 4089174877f1f3c68
parent 40890 29a45797e269
parent 40880 be44a567ed28
child 40892 6f7292b94652
merged;
     1.1 --- a/NEWS	Thu Dec 02 11:18:44 2010 -0800
     1.2 +++ b/NEWS	Thu Dec 02 21:04:20 2010 +0100
     1.3 @@ -34,8 +34,8 @@
     1.4  
     1.5  * Various options that affect pretty printing etc. are now properly
     1.6  handled within the context via configuration options, instead of
     1.7 -unsynchronized references.  There are both ML Config.T entities and
     1.8 -Isar declaration attributes to access these.
     1.9 +unsynchronized references or print modes.  There are both ML Config.T
    1.10 +entities and Isar declaration attributes to access these.
    1.11  
    1.12    ML (Config.T)                 Isar (attribute)
    1.13  
    1.14 @@ -45,6 +45,7 @@
    1.15    show_types                    show_types
    1.16    show_question_marks           show_question_marks
    1.17    show_consts                   show_consts
    1.18 +  show_abbrevs                  show_abbrevs
    1.19  
    1.20    Syntax.ambiguity_level        syntax_ambiguity_level
    1.21  
    1.22 @@ -59,6 +60,14 @@
    1.23  
    1.24  Note that corresponding "..._default" references in ML may be only
    1.25  changed globally at the ROOT session setup, but *not* within a theory.
    1.26 +The option "show_abbrevs" supersedes the former print mode
    1.27 +"no_abbrevs" with inverted meaning.
    1.28 +
    1.29 +* More systematic naming of some configuration options.
    1.30 +  INCOMPATIBILTY.
    1.31 +
    1.32 +  trace_simp  ~>  simp_trace
    1.33 +  debug_simp  ~>  simp_debug
    1.34  
    1.35  
    1.36  *** Pure ***
     2.1 --- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Thu Dec 02 11:18:44 2010 -0800
     2.2 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Thu Dec 02 21:04:20 2010 +0100
     2.3 @@ -339,6 +339,9 @@
     2.4    \item @{antiquotation_option_def show_structs}~@{text "= bool"}
     2.5    controls printing of implicit structures.
     2.6  
     2.7 +  \item @{antiquotation_option_def show_abbrevs}~@{text "= bool"}
     2.8 +  controls folding of abbreviations.
     2.9 +
    2.10    \item @{antiquotation_option_def long_names}~@{text "= bool"} forces
    2.11    names of types and constants etc.\ to be printed in their fully
    2.12    qualified internal form.
     3.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Dec 02 11:18:44 2010 -0800
     3.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Dec 02 21:04:20 2010 +0100
     3.3 @@ -99,6 +99,7 @@
     3.4      @{index_ML show_types: "bool Config.T"} & default @{ML false} \\
     3.5      @{index_ML show_sorts: "bool Config.T"} & default @{ML false} \\
     3.6      @{index_ML show_consts: "bool Config.T"} & default @{ML false} \\
     3.7 +    @{index_ML show_abbrevs: "bool Config.T"} & default @{ML true} \\
     3.8      @{index_ML long_names: "bool Unsynchronized.ref"} & default @{ML false} \\
     3.9      @{index_ML short_names: "bool Unsynchronized.ref"} & default @{ML false} \\
    3.10      @{index_ML unique_names: "bool Unsynchronized.ref"} & default @{ML true} \\
    3.11 @@ -141,6 +142,8 @@
    3.12    Note that the output can be enormous, because polymorphic constants
    3.13    often occur at several different type instances.
    3.14  
    3.15 +  \item @{ML show_abbrevs} controls folding of constant abbreviations.
    3.16 +
    3.17    \item @{ML long_names}, @{ML short_names}, and @{ML unique_names}
    3.18    control the way of printing fully qualified internal names in
    3.19    external form.  See also \secref{sec:antiq} for the document
     4.1 --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Thu Dec 02 11:18:44 2010 -0800
     4.2 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Thu Dec 02 21:04:20 2010 +0100
     4.3 @@ -357,6 +357,9 @@
     4.4    \item \indexdef{}{antiquotation option}{show\_structs}\hypertarget{antiquotation option.show-structs}{\hyperlink{antiquotation option.show-structs}{\mbox{\isa{show{\isaliteral{5F}{\isacharunderscore}}structs}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3D}{\isacharequal}}\ bool{\isaliteral{22}{\isachardoublequote}}}
     4.5    controls printing of implicit structures.
     4.6  
     4.7 +  \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}}}
     4.8 +  controls folding of abbreviations.
     4.9 +
    4.10    \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
    4.11    names of types and constants etc.\ to be printed in their fully
    4.12    qualified internal form.
     5.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Thu Dec 02 11:18:44 2010 -0800
     5.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Thu Dec 02 21:04:20 2010 +0100
     5.3 @@ -121,6 +121,7 @@
     5.4      \indexdef{}{ML}{show\_types}\verb|show_types: bool Config.T| & default \verb|false| \\
     5.5      \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool Config.T| & default \verb|false| \\
     5.6      \indexdef{}{ML}{show\_consts}\verb|show_consts: bool Config.T| & default \verb|false| \\
     5.7 +    \indexdef{}{ML}{show\_abbrevs}\verb|show_abbrevs: bool Config.T| & default \verb|true| \\
     5.8      \indexdef{}{ML}{long\_names}\verb|long_names: bool Unsynchronized.ref| & default \verb|false| \\
     5.9      \indexdef{}{ML}{short\_names}\verb|short_names: bool Unsynchronized.ref| & default \verb|false| \\
    5.10      \indexdef{}{ML}{unique\_names}\verb|unique_names: bool Unsynchronized.ref| & default \verb|true| \\
    5.11 @@ -162,6 +163,8 @@
    5.12    Note that the output can be enormous, because polymorphic constants
    5.13    often occur at several different type instances.
    5.14  
    5.15 +  \item \verb|show_abbrevs| controls folding of constant abbreviations.
    5.16 +
    5.17    \item \verb|long_names|, \verb|short_names|, and \verb|unique_names|
    5.18    control the way of printing fully qualified internal names in
    5.19    external form.  See also \secref{sec:antiq} for the document
     6.1 --- a/doc-src/TutorialI/Misc/simp.thy	Thu Dec 02 11:18:44 2010 -0800
     6.2 +++ b/doc-src/TutorialI/Misc/simp.thy	Thu Dec 02 21:04:20 2010 +0100
     6.3 @@ -422,7 +422,7 @@
     6.4  
     6.5  (*<*)lemma "x=x"
     6.6  (*>*)
     6.7 -using [[trace_simp=true]]
     6.8 +using [[simp_trace=true]]
     6.9  apply simp
    6.10  (*<*)oops(*>*)
    6.11  
     7.1 --- a/doc-src/TutorialI/Recdef/Nested2.thy	Thu Dec 02 11:18:44 2010 -0800
     7.2 +++ b/doc-src/TutorialI/Recdef/Nested2.thy	Thu Dec 02 21:04:20 2010 +0100
     7.3 @@ -30,7 +30,7 @@
     7.4  text{*\noindent
     7.5  If the proof of the induction step mystifies you, we recommend that you go through
     7.6  the chain of simplification steps in detail; you will probably need the help of
     7.7 -@{text"trace_simp"}. Theorem @{thm[source]map_cong} is discussed below.
     7.8 +@{text"simp_trace"}. Theorem @{thm[source]map_cong} is discussed below.
     7.9  %\begin{quote}
    7.10  %{term[display]"trev(trev(App f ts))"}\\
    7.11  %{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\
     8.1 --- a/src/HOL/Isar_Examples/Hoare.thy	Thu Dec 02 11:18:44 2010 -0800
     8.2 +++ b/src/HOL/Isar_Examples/Hoare.thy	Thu Dec 02 21:04:20 2010 +0100
     8.3 @@ -16,8 +16,7 @@
     8.4  text {* The following abstract syntax and semantics of Hoare Logic
     8.5    over \texttt{WHILE} programs closely follows the existing tradition
     8.6    in Isabelle/HOL of formalizing the presentation given in
     8.7 -  \cite[\S6]{Winskel:1993}.  See also
     8.8 -  \url{http://isabelle.in.tum.de/library/Hoare/} and
     8.9 +  \cite[\S6]{Winskel:1993}.  See also @{file "~~/src/HOL/Hoare"} and
    8.10    \cite{Nipkow:1998:Winskel}. *}
    8.11  
    8.12  types
    8.13 @@ -364,7 +363,7 @@
    8.14  
    8.15  text {* We now load the \emph{original} ML file for proof scripts and
    8.16    tactic definition for the Hoare Verification Condition Generator
    8.17 -  (see \url{http://isabelle.in.tum.de/library/Hoare/}).  As far as we
    8.18 +  (see @{file "~~/src/HOL/Hoare/"}).  As far as we
    8.19    are concerned here, the result is a proof method \name{hoare}, which
    8.20    may be applied to a Hoare Logic assertion to extract purely logical
    8.21    verification conditions.  It is important to note that the method
     9.1 --- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Thu Dec 02 11:18:44 2010 -0800
     9.2 +++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy	Thu Dec 02 21:04:20 2010 +0100
     9.3 @@ -10,9 +10,7 @@
     9.4  begin
     9.5  
     9.6  text {* The Mutilated Checker Board Problem, formalized inductively.
     9.7 -  See \cite{paulson-mutilated-board} and
     9.8 -  \url{http://isabelle.in.tum.de/library/HOL/Induct/Mutil.html} for
     9.9 -  the original tactic script version. *}
    9.10 +  See \cite{paulson-mutilated-board} for the original tactic script version. *}
    9.11  
    9.12  subsection {* Tilings *}
    9.13  
    10.1 --- a/src/HOL/Isar_Examples/Summation.thy	Thu Dec 02 11:18:44 2010 -0800
    10.2 +++ b/src/HOL/Isar_Examples/Summation.thy	Thu Dec 02 21:04:20 2010 +0100
    10.3 @@ -8,11 +8,6 @@
    10.4  imports Main
    10.5  begin
    10.6  
    10.7 -text_raw {* \footnote{This example is somewhat reminiscent of the
    10.8 -  \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, which is
    10.9 -  discussed in \cite{isabelle-ref} in the context of permutative
   10.10 -  rewrite rules and ordered rewriting.} *}
   10.11 -
   10.12  text {* Subsequently, we prove some summation laws of natural numbers
   10.13    (including odds, squares, and cubes).  These examples demonstrate
   10.14    how plain natural deduction (including induction) may be combined
   10.15 @@ -126,8 +121,8 @@
   10.16  qed
   10.17  
   10.18  text {* Comparing these examples with the tactic script version
   10.19 -  \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, we note
   10.20 -  an important difference of how induction vs.\ simplification is
   10.21 +  @{file "~~/src/HOL/ex/NatSum.thy"}, we note an important difference
   10.22 +  of how induction vs.\ simplification is
   10.23    applied.  While \cite[\S10]{isabelle-ref} advises for these examples
   10.24    that ``induction should not be applied until the goal is in the
   10.25    simplest form'' this would be a very bad idea in our setting.
    11.1 --- a/src/HOL/Tools/nat_numeral_simprocs.ML	Thu Dec 02 11:18:44 2010 -0800
    11.2 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Thu Dec 02 21:04:20 2010 +0100
    11.3 @@ -446,7 +446,7 @@
    11.4  (*examples:
    11.5  print_depth 22;
    11.6  set timing;
    11.7 -set trace_simp;
    11.8 +set simp_trace;
    11.9  fun test s = (Goal s; by (Simp_tac 1));
   11.10  
   11.11  (*cancel_numerals*)
    12.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Thu Dec 02 11:18:44 2010 -0800
    12.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Thu Dec 02 21:04:20 2010 +0100
    12.3 @@ -764,7 +764,7 @@
    12.4  (*examples:
    12.5  print_depth 22;
    12.6  set timing;
    12.7 -set trace_simp;
    12.8 +set simp_trace;
    12.9  fun test s = (Goal s, by (Simp_tac 1));
   12.10  
   12.11  test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)";
   12.12 @@ -803,7 +803,7 @@
   12.13  (*examples:
   12.14  print_depth 22;
   12.15  set timing;
   12.16 -set trace_simp;
   12.17 +set simp_trace;
   12.18  fun test s = (Goal s; by (Simp_tac 1));
   12.19  
   12.20  test "9*x = 12 * (y::int)";
   12.21 @@ -873,7 +873,7 @@
   12.22  (*examples:
   12.23  print_depth 22;
   12.24  set timing;
   12.25 -set trace_simp;
   12.26 +set simp_trace;
   12.27  fun test s = (Goal s; by (Asm_simp_tac 1));
   12.28  
   12.29  test "x*k = k*(y::int)";
   12.30 @@ -890,7 +890,7 @@
   12.31  (*And the same examples for fields such as rat or real:
   12.32  print_depth 22;
   12.33  set timing;
   12.34 -set trace_simp;
   12.35 +set simp_trace;
   12.36  fun test s = (Goal s; by (Asm_simp_tac 1));
   12.37  
   12.38  test "x*k = k*(y::rat)";
    13.1 --- a/src/Pure/Isar/attrib.ML	Thu Dec 02 11:18:44 2010 -0800
    13.2 +++ b/src/Pure/Isar/attrib.ML	Thu Dec 02 21:04:20 2010 +0100
    13.3 @@ -405,6 +405,7 @@
    13.4    register_config Syntax.show_question_marks_raw #>
    13.5    register_config Syntax.ambiguity_level_raw #>
    13.6    register_config Syntax.eta_contract_raw #>
    13.7 +  register_config ProofContext.show_abbrevs_raw #>
    13.8    register_config Goal_Display.goals_limit_raw #>
    13.9    register_config Goal_Display.show_main_goal_raw #>
   13.10    register_config Goal_Display.show_consts_raw #>
   13.11 @@ -415,7 +416,7 @@
   13.12    register_config Unify.trace_simp_raw #>
   13.13    register_config Unify.trace_types_raw #>
   13.14    register_config MetaSimplifier.simp_depth_limit_raw #>
   13.15 -  register_config MetaSimplifier.debug_simp_raw #>
   13.16 -  register_config MetaSimplifier.trace_simp_raw));
   13.17 +  register_config MetaSimplifier.simp_debug_raw #>
   13.18 +  register_config MetaSimplifier.simp_trace_raw));
   13.19  
   13.20  end;
    14.1 --- a/src/Pure/Isar/proof_context.ML	Thu Dec 02 11:18:44 2010 -0800
    14.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Dec 02 21:04:20 2010 +0100
    14.3 @@ -70,6 +70,8 @@
    14.4    val read_term_pattern: Proof.context -> string -> term
    14.5    val read_term_schematic: Proof.context -> string -> term
    14.6    val read_term_abbrev: Proof.context -> string -> term
    14.7 +  val show_abbrevs_raw: Config.raw
    14.8 +  val show_abbrevs: bool Config.T
    14.9    val expand_abbrevs: Proof.context -> term -> term
   14.10    val cert_term: Proof.context -> term -> term
   14.11    val cert_prop: Proof.context -> term -> term
   14.12 @@ -554,6 +556,8 @@
   14.13  
   14.14  end;
   14.15  
   14.16 +val show_abbrevs_raw = Config.declare "show_abbrevs" (fn _ => Config.Bool true);
   14.17 +val show_abbrevs = Config.bool show_abbrevs_raw;
   14.18  
   14.19  fun contract_abbrevs ctxt t =
   14.20    let
   14.21 @@ -563,7 +567,7 @@
   14.22      val retrieve = Consts.retrieve_abbrevs consts (print_mode_value () @ [""]);
   14.23      fun match_abbrev u = Option.map #1 (get_first (Pattern.match_rew thy u) (retrieve u));
   14.24    in
   14.25 -    if abbrev orelse print_mode_active "no_abbrevs" orelse not (can Term.type_of t) then t
   14.26 +    if abbrev orelse not (Config.get ctxt show_abbrevs) orelse not (can Term.type_of t) then t
   14.27      else Pattern.rewrite_term_top thy [] [match_abbrev] t
   14.28    end;
   14.29  
   14.30 @@ -1480,3 +1484,5 @@
   14.31  
   14.32  end;
   14.33  
   14.34 +val show_abbrevs = ProofContext.show_abbrevs;
   14.35 +
    15.1 --- a/src/Pure/ProofGeneral/preferences.ML	Thu Dec 02 11:18:44 2010 -0800
    15.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Thu Dec 02 21:04:20 2010 +0100
    15.3 @@ -147,10 +147,10 @@
    15.4      "Show leading question mark of variable name"];
    15.5  
    15.6  val tracing_preferences =
    15.7 - [bool_pref trace_simp_default
    15.8 + [bool_pref simp_trace_default
    15.9      "trace-simplifier"
   15.10      "Trace simplification rules.",
   15.11 -  nat_pref trace_simp_depth_limit
   15.12 +  nat_pref simp_trace_depth_limit
   15.13      "trace-simplifier-depth"
   15.14      "Trace simplifier depth limit.",
   15.15    bool_pref trace_rules
    16.1 --- a/src/Pure/Thy/thy_output.ML	Thu Dec 02 11:18:44 2010 -0800
    16.2 +++ b/src/Pure/Thy/thy_output.ML	Thu Dec 02 21:04:20 2010 +0100
    16.3 @@ -449,6 +449,7 @@
    16.4  val _ = add_option "show_sorts" (Config.put show_sorts o boolean);
    16.5  val _ = add_option "show_structs" (Config.put show_structs o boolean);
    16.6  val _ = add_option "show_question_marks" (Config.put show_question_marks o boolean);
    16.7 +val _ = add_option "show_abbrevs" (Config.put show_abbrevs o boolean);
    16.8  val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean);
    16.9  val _ = add_option "short_names" (add_wrapper o setmp_CRITICAL Name_Space.short_names o boolean);
   16.10  val _ = add_option "unique_names" (add_wrapper o setmp_CRITICAL Name_Space.unique_names o boolean);
    17.1 --- a/src/Pure/meta_simplifier.ML	Thu Dec 02 11:18:44 2010 -0800
    17.2 +++ b/src/Pure/meta_simplifier.ML	Thu Dec 02 21:04:20 2010 +0100
    17.3 @@ -11,12 +11,12 @@
    17.4  
    17.5  signature BASIC_META_SIMPLIFIER =
    17.6  sig
    17.7 -  val debug_simp: bool Config.T
    17.8 -  val debug_simp_raw: Config.raw
    17.9 -  val trace_simp: bool Config.T
   17.10 -  val trace_simp_raw: Config.raw
   17.11 -  val trace_simp_default: bool Unsynchronized.ref
   17.12 -  val trace_simp_depth_limit: int Unsynchronized.ref
   17.13 +  val simp_debug: bool Config.T
   17.14 +  val simp_debug_raw: Config.raw
   17.15 +  val simp_trace: bool Config.T
   17.16 +  val simp_trace_raw: Config.raw
   17.17 +  val simp_trace_default: bool Unsynchronized.ref
   17.18 +  val simp_trace_depth_limit: int Unsynchronized.ref
   17.19    type rrule
   17.20    val eq_rrule: rrule * rrule -> bool
   17.21    type simpset
   17.22 @@ -253,18 +253,18 @@
   17.23  val simp_depth_limit_raw = Config.declare "simp_depth_limit" (K (Config.Int 100));
   17.24  val simp_depth_limit = Config.int simp_depth_limit_raw;
   17.25  
   17.26 -val trace_simp_depth_limit = Unsynchronized.ref 1;
   17.27 +val simp_trace_depth_limit = Unsynchronized.ref 1;
   17.28  
   17.29  fun trace_depth (Simpset ({depth = (depth, exceeded), ...}, _)) msg =
   17.30 -  if depth > ! trace_simp_depth_limit then
   17.31 -    if ! exceeded then () else (tracing "trace_simp_depth_limit exceeded!"; exceeded := true)
   17.32 +  if depth > ! simp_trace_depth_limit then
   17.33 +    if ! exceeded then () else (tracing "simp_trace_depth_limit exceeded!"; exceeded := true)
   17.34    else
   17.35      (tracing (enclose "[" "]" (string_of_int depth) ^ msg); exceeded := false);
   17.36  
   17.37  val inc_simp_depth = map_simpset1 (fn (rules, prems, bounds, (depth, exceeded), context) =>
   17.38    (rules, prems, bounds,
   17.39      (depth + 1,
   17.40 -      if depth = ! trace_simp_depth_limit then Unsynchronized.ref false else exceeded), context));
   17.41 +      if depth = ! simp_trace_depth_limit then Unsynchronized.ref false else exceeded), context));
   17.42  
   17.43  fun simp_depth (Simpset ({depth = (depth, _), ...}, _)) = depth;
   17.44  
   17.45 @@ -273,12 +273,12 @@
   17.46  
   17.47  exception SIMPLIFIER of string * thm;
   17.48  
   17.49 -val debug_simp_raw = Config.declare "debug_simp" (K (Config.Bool false));
   17.50 -val debug_simp = Config.bool debug_simp_raw;
   17.51 +val simp_debug_raw = Config.declare "simp_debug" (K (Config.Bool false));
   17.52 +val simp_debug = Config.bool simp_debug_raw;
   17.53  
   17.54 -val trace_simp_default = Unsynchronized.ref false;
   17.55 -val trace_simp_raw = Config.declare "trace_simp" (fn _ => Config.Bool (! trace_simp_default));
   17.56 -val trace_simp = Config.bool trace_simp_raw;
   17.57 +val simp_trace_default = Unsynchronized.ref false;
   17.58 +val simp_trace_raw = Config.declare "simp_trace" (fn _ => Config.Bool (! simp_trace_default));
   17.59 +val simp_trace = Config.bool simp_trace_raw;
   17.60  
   17.61  fun if_enabled (Simpset ({context, ...}, _)) flag f =
   17.62    (case context of
   17.63 @@ -303,27 +303,27 @@
   17.64  
   17.65  fun print_term ss warn a t ctxt = prnt ss warn (a () ^ "\n" ^
   17.66    Syntax.string_of_term ctxt
   17.67 -    (if Config.get ctxt debug_simp then t else show_bounds ss t));
   17.68 +    (if Config.get ctxt simp_debug then t else show_bounds ss t));
   17.69  
   17.70  in
   17.71  
   17.72  fun print_term_global ss warn a thy t =
   17.73    print_term ss warn (K a) t (ProofContext.init_global thy);
   17.74  
   17.75 -fun debug warn a ss = if_enabled ss debug_simp (fn _ => prnt ss warn (a ()));
   17.76 -fun trace warn a ss = if_enabled ss trace_simp (fn _ => prnt ss warn (a ()));
   17.77 +fun debug warn a ss = if_enabled ss simp_debug (fn _ => prnt ss warn (a ()));
   17.78 +fun trace warn a ss = if_enabled ss simp_trace (fn _ => prnt ss warn (a ()));
   17.79  
   17.80 -fun debug_term warn a ss t = if_enabled ss debug_simp (print_term ss warn a t);
   17.81 -fun trace_term warn a ss t = if_enabled ss trace_simp (print_term ss warn a t);
   17.82 +fun debug_term warn a ss t = if_enabled ss simp_debug (print_term ss warn a t);
   17.83 +fun trace_term warn a ss t = if_enabled ss simp_trace (print_term ss warn a t);
   17.84  
   17.85  fun trace_cterm warn a ss ct =
   17.86 -  if_enabled ss trace_simp (print_term ss warn a (Thm.term_of ct));
   17.87 +  if_enabled ss simp_trace (print_term ss warn a (Thm.term_of ct));
   17.88  
   17.89  fun trace_thm a ss th =
   17.90 -  if_enabled ss trace_simp (print_term ss false a (Thm.full_prop_of th));
   17.91 +  if_enabled ss simp_trace (print_term ss false a (Thm.full_prop_of th));
   17.92  
   17.93  fun trace_named_thm a ss (th, name) =
   17.94 -  if_enabled ss trace_simp (print_term ss false
   17.95 +  if_enabled ss simp_trace (print_term ss false
   17.96      (fn () => if name = "" then a () else a () ^ " " ^ quote name ^ ":")
   17.97      (Thm.full_prop_of th));
   17.98  
    18.1 --- a/src/ZF/arith_data.ML	Thu Dec 02 11:18:44 2010 -0800
    18.2 +++ b/src/ZF/arith_data.ML	Thu Dec 02 21:04:20 2010 +0100
    18.3 @@ -223,7 +223,7 @@
    18.4  (*examples:
    18.5  print_depth 22;
    18.6  set timing;
    18.7 -set trace_simp;
    18.8 +set simp_trace;
    18.9  fun test s = (Goal s; by (Asm_simp_tac 1));
   18.10  
   18.11  test "x #+ y = x #+ z";
    19.1 --- a/src/ZF/int_arith.ML	Thu Dec 02 11:18:44 2010 -0800
    19.2 +++ b/src/ZF/int_arith.ML	Thu Dec 02 21:04:20 2010 +0100
    19.3 @@ -312,7 +312,7 @@
    19.4  (*
    19.5  print_depth 22;
    19.6  set timing;
    19.7 -set trace_simp;
    19.8 +set simp_trace;
    19.9  fun test s = (Goal s; by (Asm_simp_tac 1));
   19.10  val sg = #sign (rep_thm (topthm()));
   19.11  val t = FOLogic.dest_Trueprop (Logic.strip_assums_concl(getgoal 1));