src/HOL/Tools/record.ML

   val record_ex_sel_eq_simproc: simproc
   val record_split_tac: int -> tactic
   val record_split_simp_tac: thm list -> (term -> int) -> int -> tactic
   val record_split_name: string
   val record_split_wrapper: string * wrapper
-  val print_record_type_abbr: bool ref
-  val print_record_type_as_fields: bool ref
+  val print_record_type_abbr: bool Unsynchronized.ref
+  val print_record_type_as_fields: bool Unsynchronized.ref
 end;
 
 signature RECORD =
 sig
   include BASIC_RECORD
-  val timing: bool ref
-  val record_quick_and_dirty_sensitive: bool ref
+  val timing: bool Unsynchronized.ref
+  val record_quick_and_dirty_sensitive: bool Unsynchronized.ref
   val updateN: string
   val updN: string
   val ext_typeN: string
   val extN: string
   val makeN: string

     tracing (str ^ Syntax.string_of_term_global Pure.thy t);
 
 
 (* timing *)
 
-val timing = ref false;
+val timing = Unsynchronized.ref false;
 fun timeit_msg s x = if !timing then (warning s; timeit x) else x ();
 fun timing_msg s = if !timing then warning s else ();
 
 
 (* syntax *)

   ("_record_type_scheme",adv_record_type_scheme_tr)];
 
 
 (* print translations *)
 
-val print_record_type_abbr = ref true;
-val print_record_type_as_fields = ref true;
+val print_record_type_abbr = Unsynchronized.ref true;
+val print_record_type_as_fields = Unsynchronized.ref true;
 
 fun gen_field_upds_tr' mark sfx (tm as Const (name_field, _) $ k $ u) =
   let val t = (case k of (Abs (_,_,(Abs (_,_,t)$Bound 0))) 
                   => if null (loose_bnos t) then t else raise Match
                | Abs (x,_,t) => if null (loose_bnos t) then t else raise Match

 
 
 
 (** record simprocs **)
 
-val record_quick_and_dirty_sensitive = ref false;
+val record_quick_and_dirty_sensitive = Unsynchronized.ref false;
 
 
 fun quick_and_dirty_prove stndrd thy asms prop tac =
   if !record_quick_and_dirty_sensitive andalso !quick_and_dirty
   then Goal.prove (ProofContext.init thy) [] []