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

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

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun Mar 28 12:50:38 2010 -0700
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Mar 29 01:07:01 2010 -0700
     3.3 @@ -28,9 +28,10 @@
     3.4  fun only_relevance_override ns : relevance_override =
     3.5    {add = ns, del = [], only = true}
     3.6  val default_relevance_override = add_to_relevance_override []
     3.7 -fun merge_relevance_override_pairwise r1 r2 : relevance_override =
     3.8 +fun merge_relevance_override_pairwise (r1 : relevance_override)
     3.9 +                                      (r2 : relevance_override) =
    3.10    {add = #add r1 @ #add r2, del = #del r1 @ #del r2,
    3.11 -   only = #only r1 orelse #only r2} 
    3.12 +   only = #only r1 orelse #only r2}
    3.13  fun merge_relevance_overrides rs =
    3.14    fold merge_relevance_override_pairwise rs default_relevance_override
    3.15  

     4.1 --- a/src/Pure/Isar/local_theory.ML	Sun Mar 28 12:50:38 2010 -0700
     4.2 +++ b/src/Pure/Isar/local_theory.ML	Mon Mar 29 01:07:01 2010 -0700
     4.3 @@ -20,7 +20,6 @@
     4.4    val target_of: local_theory -> Proof.context
     4.5    val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
     4.6    val raw_theory: (theory -> theory) -> local_theory -> local_theory
     4.7 -  val checkpoint: local_theory -> local_theory
     4.8    val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
     4.9    val theory: (theory -> theory) -> local_theory -> local_theory
    4.10    val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
    4.11 @@ -149,7 +148,8 @@
    4.12      thy
    4.13      |> Sign.map_naming (K (naming_of lthy))
    4.14      |> f
    4.15 -    ||> Sign.restore_naming thy);
    4.16 +    ||> Sign.restore_naming thy
    4.17 +    ||> Theory.checkpoint);
    4.18  
    4.19  fun theory f = #2 o theory_result (f #> pair ());
    4.20  

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

     6.1 --- a/src/Pure/meta_simplifier.ML	Sun Mar 28 12:50:38 2010 -0700
     6.2 +++ b/src/Pure/meta_simplifier.ML	Mon Mar 29 01:07:01 2010 -0700
     6.3 @@ -15,7 +15,7 @@
     6.4    val debug_simp_value: Config.value Config.T
     6.5    val trace_simp: bool Config.T
     6.6    val trace_simp_value: Config.value Config.T
     6.7 -  val trace_simp_ref: bool Unsynchronized.ref
     6.8 +  val trace_simp_default: bool Unsynchronized.ref
     6.9    val trace_simp_depth_limit: int Unsynchronized.ref
    6.10    type rrule
    6.11    val eq_rrule: rrule * rrule -> bool
    6.12 @@ -277,9 +277,10 @@
    6.13  val debug_simp_value = Config.declare false "debug_simp" (K (Config.Bool false));
    6.14  val debug_simp = Config.bool debug_simp_value;
    6.15  
    6.16 -val trace_simp_value = Config.declare false "trace_simp" (K (Config.Bool false));
    6.17 +val trace_simp_default = Unsynchronized.ref false;
    6.18 +val trace_simp_value =
    6.19 +  Config.declare false "trace_simp" (fn _ => Config.Bool (!trace_simp_default));
    6.20  val trace_simp = Config.bool trace_simp_value;
    6.21 -val trace_simp_ref = Unsynchronized.ref false;
    6.22  
    6.23  local
    6.24  
    6.25 @@ -301,31 +302,25 @@
    6.26  fun print_term_global ss warn a thy t =
    6.27    print_term ss warn (K a) t (ProofContext.init thy);
    6.28  
    6.29 -fun if_enabled (Simpset ({context, ...}, _)) b flag f =
    6.30 +fun if_enabled (Simpset ({context, ...}, _)) flag f =
    6.31    (case context of
    6.32 -    SOME ctxt => if b orelse Config.get ctxt flag then f ctxt else ()
    6.33 +    SOME ctxt => if Config.get ctxt flag then f ctxt else ()
    6.34    | NONE => ())
    6.35  
    6.36 -fun debug warn a ss =
    6.37 -  if_enabled ss false debug_simp (fn _ => prnt ss warn (a ()));
    6.38 -fun trace warn a ss =
    6.39 -  if_enabled ss (!trace_simp_ref) trace_simp (fn _ => prnt ss warn (a ()));
    6.40 +fun debug warn a ss = if_enabled ss debug_simp (fn _ => prnt ss warn (a ()));
    6.41 +fun trace warn a ss = if_enabled ss trace_simp (fn _ => prnt ss warn (a ()));
    6.42  
    6.43 -fun debug_term warn a ss t =
    6.44 -  if_enabled ss false debug_simp (print_term ss warn a t);
    6.45 -fun trace_term warn a ss t =
    6.46 -  if_enabled ss (!trace_simp_ref) trace_simp (print_term ss warn a t);
    6.47 +fun debug_term warn a ss t = if_enabled ss debug_simp (print_term ss warn a t);
    6.48 +fun trace_term warn a ss t = if_enabled ss trace_simp (print_term ss warn a t);
    6.49  
    6.50  fun trace_cterm warn a ss ct =
    6.51 -  if_enabled ss (!trace_simp_ref) trace_simp
    6.52 -    (print_term ss warn a (Thm.term_of ct));
    6.53 +  if_enabled ss trace_simp (print_term ss warn a (Thm.term_of ct));
    6.54  
    6.55  fun trace_thm a ss th =
    6.56 -  if_enabled ss (!trace_simp_ref) trace_simp
    6.57 -    (print_term ss false a (Thm.full_prop_of th));
    6.58 +  if_enabled ss trace_simp (print_term ss false a (Thm.full_prop_of th));
    6.59  
    6.60  fun trace_named_thm a ss (th, name) =
    6.61 -  if_enabled ss (!trace_simp_ref) trace_simp (print_term ss false
    6.62 +  if_enabled ss trace_simp (print_term ss false
    6.63      (fn () => if name = "" then a () else a () ^ " " ^ quote name ^ ":")
    6.64      (Thm.full_prop_of th));
    6.65