--- a/src/Pure/Concurrent/synchronized.ML Fri Apr 08 22:48:25 2016 +0200
+++ b/src/Pure/Concurrent/synchronized.ML Sat Apr 09 11:21:38 2016 +0200
@@ -56,7 +56,7 @@
end;
in try_change () end);
-fun guarded_access var f = the (timed_access var (K NONE) f);
+fun guarded_access var f = the (timed_access var (fn _ => NONE) f);
(* unconditional change *)
@@ -66,9 +66,4 @@
end;
-
-(* toplevel pretty printing *)
-
-val _ = ML_system_pp (fn depth => fn pretty => fn var => pretty (value var, depth));
-
end;