src/HOL/Nominal/nominal_thmdecls.ML

   val eqvt_force_add: attribute
   val eqvt_force_del: attribute
   val setup: theory -> theory
   val get_eqvt_thms: Proof.context -> thm list
 
-  val NOMINAL_EQVT_DEBUG : bool ref
+  val NOMINAL_EQVT_DEBUG : bool Unsynchronized.ref
 end;
 
 structure NominalThmDecls: NOMINAL_THMDECLS =
 struct
 

 (* the implicational case it is also checked that the variables and permutation fit  *)
 (* together, i.e. are of the right "pt_class", so that a stronger version of the     *)
 (* equality-lemma can be derived. *)
 exception EQVT_FORM of string
 
-val NOMINAL_EQVT_DEBUG = ref false
+val NOMINAL_EQVT_DEBUG = Unsynchronized.ref false
 
 fun tactic (msg, tac) =
   if !NOMINAL_EQVT_DEBUG
   then tac THEN' (K (print_tac ("after " ^ msg)))
   else tac