--- a/Prove.thy	Sun Oct 25 00:14:40 2009 +0200
+++ b/Prove.thy	Sun Oct 25 01:15:03 2009 +0200
@@ -3,7 +3,7 @@
 begin
 
 ML {*
-val r = ref (NONE:(unit -> term) option)
+val r = Unsynchronized.ref (NONE:(unit -> term) option)
 *}
 
 ML {*