if_svc_enabled;
authorwenzelm
Fri Aug 20 15:41:53 1999 +0200 (1999-08-20)
changeset 730494c6f8f07631
parent 7303 96bc013c8987
child 7305 dad3b686941c
if_svc_enabled;
src/HOL/SVC_Oracle.ML
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/SVC_Oracle.ML	Fri Aug 20 15:41:19 1999 +0200
     1.2 +++ b/src/HOL/SVC_Oracle.ML	Fri Aug 20 15:41:53 1999 +0200
     1.3 @@ -102,5 +102,6 @@
     1.4  end;
     1.5  
     1.6  
     1.7 -(*True if SVC appears to exist*)
     1.8 -fun svc_enabled() = getenv "SVC_HOME" <> "";
     1.9 +(*check if user has SVC installed*)
    1.10 +fun svc_enabled () = getenv "SVC_HOME" <> "";
    1.11 +fun if_svc_enabled f x = if svc_enabled () then f x else ();
     2.1 --- a/src/HOL/ex/ROOT.ML	Fri Aug 20 15:41:19 1999 +0200
     2.2 +++ b/src/HOL/ex/ROOT.ML	Fri Aug 20 15:41:53 1999 +0200
     2.3 @@ -34,8 +34,7 @@
     2.4  time_use_thy "StringEx";
     2.5  time_use_thy "BinEx";
     2.6  
     2.7 -if svc_enabled() then time_use_thy "svc_test" 
     2.8 -                 else ();
     2.9 +if_svc_enabled time_use_thy "svc_test";
    2.10  
    2.11  (*basic use of extensible records*)
    2.12  time_use_thy "MonoidGroup";