diff -r e077484d50d8 -r 2919daadba91 src/HOL/SVC_Oracle.thy
--- a/src/HOL/SVC_Oracle.thy	Tue Aug 17 19:24:00 1999 +0200
+++ b/src/HOL/SVC_Oracle.thy	Tue Aug 17 22:11:05 1999 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/SVC_Oracle
+(*  Title:      HOL/SVC_Oracle.thy
     ID:         $Id$
     Author:     Lawrence C Paulson
     Copyright   1999  University of Cambridge
@@ -8,11 +8,15 @@
 Based upon the work of Søren T. Heilmann
 *)
 
-SVC_Oracle = NatBin + (**Real?? + **)
+theory SVC_Oracle = NatBin (** + Real??**)
+files "Tools/svc_funcs.ML":
 
 consts
   (*reserved for the oracle*)
-  iff_keep, iff_unfold :: [bool, bool] => bool 
+  iff_keep :: "[bool, bool] => bool"
+  iff_unfold :: "[bool, bool] => bool"
 
-oracle svc_oracle = Svc.oracle
+oracle
+  svc_oracle = Svc.oracle
+
 end