# HG changeset patch
# User wenzelm
# Date 1159720172 -7200
# Node ID 379ce56e5dc2110028cb74030b733af9f129a578
# Parent  cc6b31c2b9a289d159a8d3ddd32e836ecf6d9b13
proper use of svc_oracle.ML;

diff -r cc6b31c2b9a2 -r 379ce56e5dc2 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