never open structure Unsynchronized (cf. "implementation" manual);
authorwenzelm
Sat, 11 May 2013 18:16:17 +0200
changeset 51931 7c517c92d315
parent 51930 52fd62618631
child 51932 f196352201d6
never open structure Unsynchronized (cf. "implementation" manual);
src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Sat May 11 16:57:18 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Sat May 11 18:16:17 2013 +0200
@@ -55,8 +55,7 @@
 
     (* handle metis preplay fail *)
     local
-      open Unsynchronized
-      val metis_fail = ref false
+      val metis_fail = Unsynchronized.ref false
     in
       fun handle_metis_fail try_metis () =
         try_metis () handle exn =>