if_svc_enabled;
authorwenzelm
Fri, 20 Aug 1999 15:41:53 +0200
changeset 7304 94c6f8f07631
parent 7303 96bc013c8987
child 7305 dad3b686941c
if_svc_enabled;
src/HOL/SVC_Oracle.ML
src/HOL/ex/ROOT.ML
--- a/src/HOL/SVC_Oracle.ML	Fri Aug 20 15:41:19 1999 +0200
+++ b/src/HOL/SVC_Oracle.ML	Fri Aug 20 15:41:53 1999 +0200
@@ -102,5 +102,6 @@
 end;
 
 
-(*True if SVC appears to exist*)
-fun svc_enabled() = getenv "SVC_HOME" <> "";
+(*check if user has SVC installed*)
+fun svc_enabled () = getenv "SVC_HOME" <> "";
+fun if_svc_enabled f x = if svc_enabled () then f x else ();
--- a/src/HOL/ex/ROOT.ML	Fri Aug 20 15:41:19 1999 +0200
+++ b/src/HOL/ex/ROOT.ML	Fri Aug 20 15:41:53 1999 +0200
@@ -34,8 +34,7 @@
 time_use_thy "StringEx";
 time_use_thy "BinEx";
 
-if svc_enabled() then time_use_thy "svc_test" 
-                 else ();
+if_svc_enabled time_use_thy "svc_test";
 
 (*basic use of extensible records*)
 time_use_thy "MonoidGroup";