src/HOL/ex/SVC_Oracle.thy

--- a/src/HOL/ex/SVC_Oracle.thy	Tue Sep 29 14:59:24 2009 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy	Tue Sep 29 16:24:36 2009 +0200
@@ -44,8 +44,8 @@
     and body   = Term.strip_all_body t
     val Us = map #2 params
     val nPar = length params
-    val vname = ref "V_a"
-    val pairs = ref ([] : (term*term) list)
+    val vname = Unsynchronized.ref "V_a"
+    val pairs = Unsynchronized.ref ([] : (term*term) list)
     fun insert t =
         let val T = fastype_of t
             val v = Logic.combound (Var ((!vname,0), Us--->T), 0, nPar)