--- a/ProgTutorial/Parsing.thy	Fri Oct 02 15:38:14 2009 +0200
+++ b/ProgTutorial/Parsing.thy	Sat Oct 03 13:01:39 2009 +0200
@@ -1089,7 +1089,7 @@
   
 *}
 
-ML_val{*val r = ref (NONE:(unit -> term) option)*}
+ML_val{*val r = Unsynchronized.ref (NONE:(unit -> term) option)*}
 ML{*let
    fun after_qed thm_name thms lthy =
         LocalTheory.note Thm.theoremK (thm_name, (flat thms)) lthy |> snd