# HG changeset patch
# User paulson
# Date 933953325 -7200
# Node ID 676027b1d770f82c53ac729e5d8752775215cbc1
# Parent  860479291bb5081f6c1cebece94466b14b16b4a1
svc_enabled is now declared as a function

diff -r 860479291bb5 -r 676027b1d770 src/HOL/SVC_Oracle.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" <> "";
diff -r 860479291bb5 -r 676027b1d770 src/HOL/ex/ROOT.ML
--- 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";