src/Tools/Compute_Oracle/linker.ML

 exception PCompute of string
 
 datatype theorem = MonoThm of thm | PolyThm of thm * Linker.instances * thm list
 datatype pattern = MonoPattern of term | PolyPattern of term * Linker.instances * term list
 
-datatype pcomputer = PComputer of theory_ref * Compute.computer * theorem list ref * pattern list ref 
+datatype pcomputer =
+  PComputer of theory_ref * Compute.computer * theorem list Unsynchronized.ref *
+    pattern list Unsynchronized.ref 
 
 (*fun collect_consts (Var x) = []
   | collect_consts (Bound _) = []
   | collect_consts (a $ b) = (collect_consts a)@(collect_consts b)
   | collect_consts (Abs (_, _, body)) = collect_consts body

 fun conv_subst thy (subst : Type.tyenv) =
     map (fn (iname, (sort, ty)) => (ctyp_of thy (TVar (iname, sort)), ctyp_of thy ty)) (Vartab.dest subst)
 
 fun add_monos thy monocs pats ths =
     let
-        val changed = ref false
+        val changed = Unsynchronized.ref false
         fun add monocs (th as (MonoThm _)) = ([], th)
           | add monocs (PolyThm (th, instances, instanceths)) =
             let
                 val (newsubsts, instances) = Linker.add_instances thy instances monocs
                 val _ = if not (null newsubsts) then changed := true else ()

 
 structure CThmtab = Table(type key = cthm val ord = cthm_ord)
 
 fun remove_duplicates ths =
     let
-        val counter = ref 0
-        val tab = ref (CThmtab.empty : unit CThmtab.table)
-        val thstab = ref (Inttab.empty : thm Inttab.table)
+        val counter = Unsynchronized.ref 0
+        val tab = Unsynchronized.ref (CThmtab.empty : unit CThmtab.table)
+        val thstab = Unsynchronized.ref (Inttab.empty : thm Inttab.table)
         fun update th =
             let
                 val key = thm2cthm th
             in
                 case CThmtab.lookup (!tab) key of

 				     ths (cs, [])
 	val pats = map create_pattern pats
 	val (_, (pats, ths)) = add_monos thy monocs pats ths
 	val computer = create_computer machine thy pats ths
     in
-	PComputer (Theory.check_thy thy, computer, ref ths, ref pats)
+	PComputer (Theory.check_thy thy, computer, Unsynchronized.ref ths, Unsynchronized.ref pats)
     end
 
 fun make machine thy ths cs = make_with_cache machine thy [] ths cs
 
 fun add_instances (PComputer (thyref, computer, rths, rpats)) cs =