src/Pure/Isar/outer_lex.ML
changeset 32738 15bb09ca0378
parent 30586 9674f64a0702
     1.1 --- a/src/Pure/Isar/outer_lex.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/Isar/outer_lex.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -83,7 +83,7 @@
     1.4  datatype slot =
     1.5    Slot |
     1.6    Value of value option |
     1.7 -  Assignable of value option ref;
     1.8 +  Assignable of value option Unsynchronized.ref;
     1.9  
    1.10  
    1.11  (* datatype token *)
    1.12 @@ -245,7 +245,7 @@
    1.13  (* static binding *)
    1.14  
    1.15  (*1st stage: make empty slots assignable*)
    1.16 -fun assignable (Token (x, y, Slot)) = Token (x, y, Assignable (ref NONE))
    1.17 +fun assignable (Token (x, y, Slot)) = Token (x, y, Assignable (Unsynchronized.ref NONE))
    1.18    | assignable tok = tok;
    1.19  
    1.20  (*2nd stage: assign values as side-effect of scanning*)
    1.21 @@ -253,7 +253,7 @@
    1.22    | assign _ _ = ();
    1.23  
    1.24  (*3rd stage: static closure of final values*)
    1.25 -fun closure (Token (x, y, Assignable (ref v))) = Token (x, y, Value v)
    1.26 +fun closure (Token (x, y, Assignable (Unsynchronized.ref v))) = Token (x, y, Value v)
    1.27    | closure tok = tok;
    1.28  
    1.29