# HG changeset patch
# User wenzelm
# Date 935156513 -7200
# Node ID 94c6f8f07631d2a9230415d97edb4162a06fb8a7
# Parent  96bc013c8987d3e46c39bbe0c354d62f498995f1
if_svc_enabled;

diff -r 96bc013c8987 -r 94c6f8f07631 src/HOL/SVC_Oracle.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 ();
diff -r 96bc013c8987 -r 94c6f8f07631 src/HOL/ex/ROOT.ML
--- 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";