diff -r 51f75d24bd73 -r 5e95387bef45 Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Thu Jan 06 14:53:38 2011 +0000
+++ b/Nominal/nominal_library.ML	Thu Jan 06 19:57:57 2011 +0000
@@ -6,6 +6,9 @@
 
 signature NOMINAL_LIBRARY =
 sig
+  val trace: bool Unsynchronized.ref
+  val trace_msg: (unit -> string) -> unit
+
   val last2: 'a list -> 'a * 'a
   val split_last2: 'a list -> 'a list * 'a * 'a
   val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list
@@ -141,6 +144,10 @@
 structure Nominal_Library: NOMINAL_LIBRARY =
 struct
 
+val trace = Unsynchronized.ref false
+fun trace_msg msg = if ! trace then tracing (msg ()) else ()
+
+
 (* orders an AList according to keys - every key needs to be there *)
 fun order eq keys list = 
   map (the o AList.lookup eq list) keys