svc_enabled is now declared as a function
authorpaulson
Fri, 06 Aug 1999 17:28:45 +0200
changeset 7187 676027b1d770
parent 7186 860479291bb5
child 7188 2bc63a44721b
svc_enabled is now declared as a function
src/HOL/SVC_Oracle.ML
src/HOL/ex/ROOT.ML
--- a/src/HOL/SVC_Oracle.ML	Fri Aug 06 17:27:51 1999 +0200
+++ b/src/HOL/SVC_Oracle.ML	Fri Aug 06 17:28:45 1999 +0200
@@ -22,3 +22,5 @@
 	| Subscript       => Seq.empty;
 
 
+(*True if SVC appears to exist*)
+fun svc_enabled() = getenv "SVC_HOME" <> "";
--- a/src/HOL/ex/ROOT.ML	Fri Aug 06 17:27:51 1999 +0200
+++ b/src/HOL/ex/ROOT.ML	Fri Aug 06 17:28:45 1999 +0200
@@ -33,7 +33,9 @@
 
 time_use_thy "StringEx";
 time_use_thy "BinEx";
-time_use_thy "svc_test";
+
+if svc_enabled() then time_use_thy "svc_test" 
+                 else ();
 
 (*basic use of extensible records*)
 time_use_thy "MonoidGroup";