1.1 --- a/src/Pure/Syntax/syn_trans.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/Syntax/syn_trans.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  signature SYN_TRANS0 =
     1.6  sig
     1.7 -  val eta_contract: bool ref
     1.8 +  val eta_contract: bool Unsynchronized.ref
     1.9    val atomic_abs_tr': string * typ * term -> term * term
    1.10    val preserve_binder_abs_tr': string -> string -> string * (term list -> term)
    1.11    val preserve_binder_abs2_tr': string -> string -> string * (term list -> term)
    1.12 @@ -276,7 +276,7 @@
    1.13  
    1.14  (*do (partial) eta-contraction before printing*)
    1.15  
    1.16 -val eta_contract = ref true;
    1.17 +val eta_contract = Unsynchronized.ref true;
    1.18  
    1.19  fun eta_contr tm =
    1.20    let