# HG changeset patch
# User wenzelm
# Date 1368288977 -7200
# Node ID 7c517c92d31525dfb2b5161cd9324007fd18f8d6
# Parent  52fd62618631b24361ae340646a1afce699b90d4
never open structure Unsynchronized (cf. "implementation" manual);

diff -r 52fd62618631 -r 7c517c92d315 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 =>