--- 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";