# HG changeset patch
# User haftmann
# Date 1433177960 -7200
# Node ID 0e6742f89c038614573cf910394da1b3e28dc711
# Parent  a808b57d5b0d244cb4013d5b21c69cb2162d8829
dedicated config options to deactivate uncheck phase for improvable syntax

diff -r a808b57d5b0d -r 0e6742f89c03 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Mon Jun 01 18:59:19 2015 +0200
+++ b/src/Pure/Isar/overloading.ML	Mon Jun 01 18:59:20 2015 +0200
@@ -11,6 +11,7 @@
   val map_improvable_syntax: (improvable_syntax -> improvable_syntax)
     -> Proof.context -> Proof.context
   val set_primary_constraints: Proof.context -> Proof.context
+  val show_reverted_improvements: bool Config.T;
 
   val overloading: (string * (string * typ) * bool) list -> theory -> local_theory
   val overloading_cmd: (string * string * bool) list -> theory -> local_theory
@@ -90,12 +91,16 @@
     NONE => NONE
   | SOME t' => if t aconv t' then NONE else SOME t');
 
+val show_reverted_improvements =
+  Attrib.setup_config_bool @{binding "show_reverted_improvements"} (K true);
+
 fun improve_term_uncheck ts ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
     val {syntax = {unchecks, ...}, ...} = Improvable_Syntax.get ctxt;
+    val revert = Config.get ctxt show_reverted_improvements;
     val ts' = map (rewrite_liberal thy unchecks) ts;
-  in if exists is_some ts' then SOME (map2 the_default ts ts', ctxt) else NONE end;
+  in if revert andalso exists is_some ts' then SOME (map2 the_default ts ts', ctxt) else NONE end;
 
 fun set_primary_constraints ctxt =
   let