src/HOL/Tools/record.ML
changeset 32740 9dd0a2f83429
parent 32335 41fe1c93f218
child 32760 ea6672bff5dd
     1.1 --- a/src/HOL/Tools/record.ML	Tue Sep 29 14:59:24 2009 +0200
     1.2 +++ b/src/HOL/Tools/record.ML	Tue Sep 29 16:24:36 2009 +0200
     1.3 @@ -15,15 +15,15 @@
     1.4    val record_split_simp_tac: thm list -> (term -> int) -> int -> tactic
     1.5    val record_split_name: string
     1.6    val record_split_wrapper: string * wrapper
     1.7 -  val print_record_type_abbr: bool ref
     1.8 -  val print_record_type_as_fields: bool ref
     1.9 +  val print_record_type_abbr: bool Unsynchronized.ref
    1.10 +  val print_record_type_as_fields: bool Unsynchronized.ref
    1.11  end;
    1.12  
    1.13  signature RECORD =
    1.14  sig
    1.15    include BASIC_RECORD
    1.16 -  val timing: bool ref
    1.17 -  val record_quick_and_dirty_sensitive: bool ref
    1.18 +  val timing: bool Unsynchronized.ref
    1.19 +  val record_quick_and_dirty_sensitive: bool Unsynchronized.ref
    1.20    val updateN: string
    1.21    val updN: string
    1.22    val ext_typeN: string
    1.23 @@ -118,7 +118,7 @@
    1.24  
    1.25  (* timing *)
    1.26  
    1.27 -val timing = ref false;
    1.28 +val timing = Unsynchronized.ref false;
    1.29  fun timeit_msg s x = if !timing then (warning s; timeit x) else x ();
    1.30  fun timing_msg s = if !timing then warning s else ();
    1.31  
    1.32 @@ -671,8 +671,8 @@
    1.33  
    1.34  (* print translations *)
    1.35  
    1.36 -val print_record_type_abbr = ref true;
    1.37 -val print_record_type_as_fields = ref true;
    1.38 +val print_record_type_abbr = Unsynchronized.ref true;
    1.39 +val print_record_type_as_fields = Unsynchronized.ref true;
    1.40  
    1.41  fun gen_field_upds_tr' mark sfx (tm as Const (name_field, _) $ k $ u) =
    1.42    let val t = (case k of (Abs (_,_,(Abs (_,_,t)$Bound 0))) 
    1.43 @@ -864,7 +864,7 @@
    1.44  
    1.45  (** record simprocs **)
    1.46  
    1.47 -val record_quick_and_dirty_sensitive = ref false;
    1.48 +val record_quick_and_dirty_sensitive = Unsynchronized.ref false;
    1.49  
    1.50  
    1.51  fun quick_and_dirty_prove stndrd thy asms prop tac =