src/HOL/ex/SVC_Oracle.thy
changeset 32740 9dd0a2f83429
parent 28290 4cc2b6046258
child 34974 18b41bba42b5
     1.1 --- a/src/HOL/ex/SVC_Oracle.thy	Tue Sep 29 14:59:24 2009 +0200
     1.2 +++ b/src/HOL/ex/SVC_Oracle.thy	Tue Sep 29 16:24:36 2009 +0200
     1.3 @@ -44,8 +44,8 @@
     1.4      and body   = Term.strip_all_body t
     1.5      val Us = map #2 params
     1.6      val nPar = length params
     1.7 -    val vname = ref "V_a"
     1.8 -    val pairs = ref ([] : (term*term) list)
     1.9 +    val vname = Unsynchronized.ref "V_a"
    1.10 +    val pairs = Unsynchronized.ref ([] : (term*term) list)
    1.11      fun insert t =
    1.12          let val T = fastype_of t
    1.13              val v = Logic.combound (Var ((!vname,0), Us--->T), 0, nPar)