src/Tools/nbe.ML
changeset 32740 9dd0a2f83429
parent 32544 e129333b9df0
child 32966 5b21661fe618
     1.1 --- a/src/Tools/nbe.ML	Tue Sep 29 14:59:24 2009 +0200
     1.2 +++ b/src/Tools/nbe.ML	Tue Sep 29 16:24:36 2009 +0200
     1.3 @@ -19,8 +19,8 @@
     1.4                                               (*abstractions as closures*)
     1.5    val same: Univ -> Univ -> bool
     1.6  
     1.7 -  val univs_ref: (unit -> Univ list -> Univ list) option ref
     1.8 -  val trace: bool ref
     1.9 +  val univs_ref: (unit -> Univ list -> Univ list) option Unsynchronized.ref
    1.10 +  val trace: bool Unsynchronized.ref
    1.11  
    1.12    val setup: theory -> theory
    1.13    val add_const_alias: thm -> theory -> theory
    1.14 @@ -31,7 +31,7 @@
    1.15  
    1.16  (* generic non-sense *)
    1.17  
    1.18 -val trace = ref false;
    1.19 +val trace = Unsynchronized.ref false;
    1.20  fun traced f x = if !trace then (tracing (f x); x) else x;
    1.21  
    1.22  
    1.23 @@ -216,7 +216,7 @@
    1.24  
    1.25  (* nbe specific syntax and sandbox communication *)
    1.26  
    1.27 -val univs_ref = ref (NONE : (unit -> Univ list -> Univ list) option);
    1.28 +val univs_ref = Unsynchronized.ref (NONE : (unit -> Univ list -> Univ list) option);
    1.29  
    1.30  local
    1.31    val prefix =      "Nbe.";