--- a/src/HOL/Tools/res_axioms.ML Fri Oct 16 00:26:19 2009 +0200
+++ b/src/HOL/Tools/res_axioms.ML Fri Oct 16 10:45:10 2009 +0200
@@ -5,6 +5,8 @@
signature RES_AXIOMS =
sig
+ val trace: bool Unsynchronized.ref
+ val trace_msg: (unit -> string) -> unit
val cnf_axiom: theory -> thm -> thm list
val pairname: thm -> string * thm
val multi_base_blacklist: string list
@@ -24,6 +26,9 @@
structure ResAxioms: RES_AXIOMS =
struct
+val trace = Unsynchronized.ref false;
+fun trace_msg msg = if ! trace then tracing (msg ()) else ();
+
(* FIXME legacy *)
fun freeze_thm th = #1 (Drule.freeze_thaw th);