src/HOL/ex/SVC_Oracle.thy

--- a/src/HOL/ex/SVC_Oracle.thy	Sun Oct 01 18:29:31 2006 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy	Sun Oct 01 18:29:32 2006 +0200
@@ -10,7 +10,7 @@
 
 theory SVC_Oracle
 imports Main
-uses "svc_funcs.ML"
+uses "svc_funcs.ML" ("svc_oracle.ML")
 begin
 
 consts
@@ -22,4 +22,6 @@
 oracle
   svc_oracle ("term") = Svc.oracle
 
+use "svc_oracle.ML"
+
 end