--- 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 *)