merged

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sun Mar 28 12:50:38 2010 -0700
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Mon Mar 29 01:07:01 2010 -0700
@@ -170,7 +170,6 @@
     if (is_inductify options) then
       let
         val lthy' = Local_Theory.theory (preprocess options t) lthy
-          |> Local_Theory.checkpoint
         val const =
           case Predicate_Compile_Fun.pred_of_function (ProofContext.theory_of lthy') const of
             SOME c => c

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Mar 28 12:50:38 2010 -0700
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 29 01:07:01 2010 -0700
@@ -2912,7 +2912,6 @@
     val const = prep_const thy raw_const
     val lthy' = Local_Theory.theory (PredData.map
         (extend (fetch_pred_data thy) (depending_preds_of thy) const)) lthy
-      |> Local_Theory.checkpoint
     val thy' = ProofContext.theory_of lthy'
     val preds = Graph.all_succs (PredData.get thy') [const] |> filter_out (has_elim thy')
     fun mk_cases const =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun Mar 28 12:50:38 2010 -0700
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Mar 29 01:07:01 2010 -0700
@@ -28,9 +28,10 @@
 fun only_relevance_override ns : relevance_override =
   {add = ns, del = [], only = true}
 val default_relevance_override = add_to_relevance_override []
-fun merge_relevance_override_pairwise r1 r2 : relevance_override =
+fun merge_relevance_override_pairwise (r1 : relevance_override)
+                                      (r2 : relevance_override) =
   {add = #add r1 @ #add r2, del = #del r1 @ #del r2,
-   only = #only r1 orelse #only r2} 
+   only = #only r1 orelse #only r2}
 fun merge_relevance_overrides rs =
   fold merge_relevance_override_pairwise rs default_relevance_override
 

--- a/src/Pure/Isar/local_theory.ML	Sun Mar 28 12:50:38 2010 -0700
+++ b/src/Pure/Isar/local_theory.ML	Mon Mar 29 01:07:01 2010 -0700
@@ -20,7 +20,6 @@
   val target_of: local_theory -> Proof.context
   val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   val raw_theory: (theory -> theory) -> local_theory -> local_theory
-  val checkpoint: local_theory -> local_theory
   val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   val theory: (theory -> theory) -> local_theory -> local_theory
   val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
@@ -149,7 +148,8 @@
     thy
     |> Sign.map_naming (K (naming_of lthy))
     |> f
-    ||> Sign.restore_naming thy);
+    ||> Sign.restore_naming thy
+    ||> Theory.checkpoint);
 
 fun theory f = #2 o theory_result (f #> pair ());
 

--- a/src/Pure/ProofGeneral/preferences.ML	Sun Mar 28 12:50:38 2010 -0700
+++ b/src/Pure/ProofGeneral/preferences.ML	Mon Mar 29 01:07:01 2010 -0700
@@ -146,7 +146,7 @@
     "Show leading question mark of variable name"];
 
 val tracing_preferences =
- [bool_pref trace_simp_ref
+ [bool_pref trace_simp_default
     "trace-simplifier"
     "Trace simplification rules.",
   nat_pref trace_simp_depth_limit

--- a/src/Pure/meta_simplifier.ML	Sun Mar 28 12:50:38 2010 -0700
+++ b/src/Pure/meta_simplifier.ML	Mon Mar 29 01:07:01 2010 -0700
@@ -15,7 +15,7 @@
   val debug_simp_value: Config.value Config.T
   val trace_simp: bool Config.T
   val trace_simp_value: Config.value Config.T
-  val trace_simp_ref: bool Unsynchronized.ref
+  val trace_simp_default: bool Unsynchronized.ref
   val trace_simp_depth_limit: int Unsynchronized.ref
   type rrule
   val eq_rrule: rrule * rrule -> bool
@@ -277,9 +277,10 @@
 val debug_simp_value = Config.declare false "debug_simp" (K (Config.Bool false));
 val debug_simp = Config.bool debug_simp_value;
 
-val trace_simp_value = Config.declare false "trace_simp" (K (Config.Bool false));
+val trace_simp_default = Unsynchronized.ref false;
+val trace_simp_value =
+  Config.declare false "trace_simp" (fn _ => Config.Bool (!trace_simp_default));
 val trace_simp = Config.bool trace_simp_value;
-val trace_simp_ref = Unsynchronized.ref false;
 
 local
 
@@ -301,31 +302,25 @@
 fun print_term_global ss warn a thy t =
   print_term ss warn (K a) t (ProofContext.init thy);
 
-fun if_enabled (Simpset ({context, ...}, _)) b flag f =
+fun if_enabled (Simpset ({context, ...}, _)) flag f =
   (case context of
-    SOME ctxt => if b orelse Config.get ctxt flag then f ctxt else ()
+    SOME ctxt => if Config.get ctxt flag then f ctxt else ()
   | NONE => ())
 
-fun debug warn a ss =
-  if_enabled ss false debug_simp (fn _ => prnt ss warn (a ()));
-fun trace warn a ss =
-  if_enabled ss (!trace_simp_ref) trace_simp (fn _ => prnt ss warn (a ()));
+fun debug warn a ss = if_enabled ss debug_simp (fn _ => prnt ss warn (a ()));
+fun trace warn a ss = if_enabled ss trace_simp (fn _ => prnt ss warn (a ()));
 
-fun debug_term warn a ss t =
-  if_enabled ss false debug_simp (print_term ss warn a t);
-fun trace_term warn a ss t =
-  if_enabled ss (!trace_simp_ref) trace_simp (print_term ss warn a t);
+fun debug_term warn a ss t = if_enabled ss debug_simp (print_term ss warn a t);
+fun trace_term warn a ss t = if_enabled ss trace_simp (print_term ss warn a t);
 
 fun trace_cterm warn a ss ct =
-  if_enabled ss (!trace_simp_ref) trace_simp
-    (print_term ss warn a (Thm.term_of ct));
+  if_enabled ss trace_simp (print_term ss warn a (Thm.term_of ct));
 
 fun trace_thm a ss th =
-  if_enabled ss (!trace_simp_ref) trace_simp
-    (print_term ss false a (Thm.full_prop_of th));
+  if_enabled ss trace_simp (print_term ss false a (Thm.full_prop_of th));
 
 fun trace_named_thm a ss (th, name) =
-  if_enabled ss (!trace_simp_ref) trace_simp (print_term ss false
+  if_enabled ss trace_simp (print_term ss false
     (fn () => if name = "" then a () else a () ^ " " ^ quote name ^ ":")
     (Thm.full_prop_of th));