tuned signature;
authorwenzelm
Wed Oct 11 22:55:14 2006 +0200 (2006-10-11)
changeset 20977dbf1eca9b34e
parent 20976 e324808e9f1f
child 20978 51956522c306
tuned signature;
src/Pure/General/secure.ML
     1.1 --- a/src/Pure/General/secure.ML	Wed Oct 11 20:35:54 2006 +0200
     1.2 +++ b/src/Pure/General/secure.ML	Wed Oct 11 22:55:14 2006 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  signature SECURE =
     1.6  sig
     1.7 -  val set_secure: unit -> bool
     1.8 +  val set_secure: unit -> unit
     1.9    val is_secure: unit -> bool
    1.10    val deny_secure: string -> unit
    1.11    val use: string -> unit
    1.12 @@ -22,7 +22,7 @@
    1.13  
    1.14  val secure = ref false;
    1.15  
    1.16 -fun set_secure () = set secure;
    1.17 +fun set_secure () = secure := true;
    1.18  fun is_secure () = ! secure;
    1.19  
    1.20  fun deny_secure msg = deny (is_secure ()) msg;