# HG changeset patch
# User wenzelm
# Date 934920665 -7200
# Node ID 2919daadba912f8887681cf0432720d848512c3e
# Parent  e077484d50d89a8297bbbe7e6da9ac242c4ee690
turned SVC_Oracle into a new-style theory in order to get automatic
  handling of its additional dependency on Tools/svc_funcs.ML;

diff -r e077484d50d8 -r 2919daadba91 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Tue Aug 17 19:24:00 1999 +0200
+++ b/src/HOL/ROOT.ML	Tue Aug 17 22:11:05 1999 +0200
@@ -75,9 +75,6 @@
 use "bin_simprocs.ML";
 cd "..";
 
-use "Tools/svc_funcs.ML";
-use_thy "SVC_Oracle";
-
 (*the all-in-one theory*)
 use_thy "Main";
 
diff -r e077484d50d8 -r 2919daadba91 src/HOL/SVC_Oracle.ML
--- a/src/HOL/SVC_Oracle.ML	Tue Aug 17 19:24:00 1999 +0200
+++ b/src/HOL/SVC_Oracle.ML	Tue Aug 17 22:11:05 1999 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/SVC_Oracle
+(*  Title:      HOL/SVC_Oracle.ML
     ID:         $Id$
     Author:     Lawrence C Paulson
     Copyright   1999  University of Cambridge
@@ -11,9 +11,11 @@
 (*Present the entire subgoal to the oracle, assumptions and all, but possibly
   abstracted.  Use via compose_tac, which performs no lifting but will
   instantiate variables.*)
+local val svc_thy = the_context () in
+
 fun svc_tac i st = 
-  let val prem = List.nth (prems_of st, i-1)
-      val th = invoke_oracle thy "svc_oracle" 
+  let val prem = BasisLibrary.List.nth (prems_of st, i-1)
+      val th = invoke_oracle svc_thy "svc_oracle"
 	             (#sign (rep_thm st), Svc.OracleExn prem)
    in 
       compose_tac (false, th, 0) i st
@@ -21,6 +23,8 @@
    handle Svc.OracleExn _ => Seq.empty
 	| Subscript       => Seq.empty;
 
+end;
+
 
 (*True if SVC appears to exist*)
 fun svc_enabled() = getenv "SVC_HOME" <> "";
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