# HG changeset patch
# User nipkow
# Date 1254408418 -7200
# Node ID 314b6a73b55cd8207f7dd550420a3a7529f2b281
# Parent  99843bbfaeb2283e40c7c614dcfb0ab173842942# Parent  712ad8109fff1bd7ce0ed43abcaf2cda3cf2a423
merged

diff -r 712ad8109fff -r 314b6a73b55c src/Tools/more_conv.ML
--- a/src/Tools/more_conv.ML	Thu Oct 01 16:46:48 2009 +0200
+++ b/src/Tools/more_conv.ML	Thu Oct 01 16:46:58 2009 +0200
@@ -46,16 +46,18 @@
   Conv.arg_conv (Conv.abs_conv (fn (_, cx) => cv cx) ctxt)
 
 
-fun cache_conv conv =   (* FIXME not thread-safe *)
-  let 
-    val tab = Unsynchronized.ref Termtab.empty
-    fun add_result t thm =
-      let val _ = Unsynchronized.change tab (Termtab.insert Thm.eq_thm (t, thm))
-      in thm end
-    fun cconv ct =  
-      (case Termtab.lookup (!tab) (Thm.term_of ct) of
+fun cache_conv conv =
+  let
+    val cache = Synchronized.var "cache_conv" Termtab.empty
+    fun lookup t =
+      Synchronized.change_result cache (fn tab => (Termtab.lookup tab t, tab))
+    val keep = Synchronized.change cache o Termtab.insert Thm.eq_thm
+    fun keep_result t thm = (keep (t, thm); thm)
+
+    fun cconv ct =
+      (case lookup (Thm.term_of ct) of
         SOME thm => thm
-      | NONE => add_result (Thm.term_of ct) (conv ct))
+      | NONE => keep_result (Thm.term_of ct) (conv ct))
   in cconv end
 
 end