--- a/src/Pure/General/secure.ML Tue Jan 01 16:09:26 2008 +0100 +++ b/src/Pure/General/secure.ML Tue Jan 01 16:09:27 2008 +0100 @@ -30,6 +30,7 @@ fun deny_secure msg = if is_secure () then error msg else (); + (** critical operations **) (* ML evaluation *)