1.1 --- a/src/HOL/ROOT.ML	Tue Aug 17 19:24:00 1999 +0200
     1.2 +++ b/src/HOL/ROOT.ML	Tue Aug 17 22:11:05 1999 +0200
     1.3 @@ -75,9 +75,6 @@
     1.4  use "bin_simprocs.ML";
     1.5  cd "..";
     1.6  
     1.7 -use "Tools/svc_funcs.ML";
     1.8 -use_thy "SVC_Oracle";
     1.9 -
    1.10  (*the all-in-one theory*)
    1.11  use_thy "Main";
    1.12  

     2.1 --- a/src/HOL/SVC_Oracle.ML	Tue Aug 17 19:24:00 1999 +0200
     2.2 +++ b/src/HOL/SVC_Oracle.ML	Tue Aug 17 22:11:05 1999 +0200
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      HOL/SVC_Oracle
     2.5 +(*  Title:      HOL/SVC_Oracle.ML
     2.6      ID:         $Id$
     2.7      Author:     Lawrence C Paulson
     2.8      Copyright   1999  University of Cambridge
     2.9 @@ -11,9 +11,11 @@
    2.10  (*Present the entire subgoal to the oracle, assumptions and all, but possibly
    2.11    abstracted.  Use via compose_tac, which performs no lifting but will
    2.12    instantiate variables.*)
    2.13 +local val svc_thy = the_context () in
    2.14 +
    2.15  fun svc_tac i st = 
    2.16 -  let val prem = List.nth (prems_of st, i-1)
    2.17 -      val th = invoke_oracle thy "svc_oracle" 
    2.18 +  let val prem = BasisLibrary.List.nth (prems_of st, i-1)
    2.19 +      val th = invoke_oracle svc_thy "svc_oracle"
    2.20  	             (#sign (rep_thm st), Svc.OracleExn prem)
    2.21     in 
    2.22        compose_tac (false, th, 0) i st
    2.23 @@ -21,6 +23,8 @@
    2.24     handle Svc.OracleExn _ => Seq.empty
    2.25  	| Subscript       => Seq.empty;
    2.26  
    2.27 +end;
    2.28 +
    2.29  
    2.30  (*True if SVC appears to exist*)
    2.31  fun svc_enabled() = getenv "SVC_HOME" <> "";

     3.1 --- a/src/HOL/SVC_Oracle.thy	Tue Aug 17 19:24:00 1999 +0200
     3.2 +++ b/src/HOL/SVC_Oracle.thy	Tue Aug 17 22:11:05 1999 +0200
     3.3 @@ -1,4 +1,4 @@
     3.4 -(*  Title:      HOL/SVC_Oracle
     3.5 +(*  Title:      HOL/SVC_Oracle.thy
     3.6      ID:         $Id$
     3.7      Author:     Lawrence C Paulson
     3.8      Copyright   1999  University of Cambridge
     3.9 @@ -8,11 +8,15 @@
    3.10  Based upon the work of Søren T. Heilmann
    3.11  *)
    3.12  
    3.13 -SVC_Oracle = NatBin + (**Real?? + **)
    3.14 +theory SVC_Oracle = NatBin (** + Real??**)
    3.15 +files "Tools/svc_funcs.ML":
    3.16  
    3.17  consts
    3.18    (*reserved for the oracle*)
    3.19 -  iff_keep, iff_unfold :: [bool, bool] => bool 
    3.20 +  iff_keep :: "[bool, bool] => bool"
    3.21 +  iff_unfold :: "[bool, bool] => bool"
    3.22  
    3.23 -oracle svc_oracle = Svc.oracle
    3.24 +oracle
    3.25 +  svc_oracle = Svc.oracle
    3.26 +
    3.27  end