src/HOL/SVC_Oracle.ML
changeset 7237 2919daadba91
parent 7187 676027b1d770
child 7284 29105299799c
     1.1 --- a/src/HOL/SVC_Oracle.ML	Tue Aug 17 19:24:00 1999 +0200
     1.2 +++ b/src/HOL/SVC_Oracle.ML	Tue Aug 17 22:11:05 1999 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOL/SVC_Oracle
     1.5 +(*  Title:      HOL/SVC_Oracle.ML
     1.6      ID:         $Id$
     1.7      Author:     Lawrence C Paulson
     1.8      Copyright   1999  University of Cambridge
     1.9 @@ -11,9 +11,11 @@
    1.10  (*Present the entire subgoal to the oracle, assumptions and all, but possibly
    1.11    abstracted.  Use via compose_tac, which performs no lifting but will
    1.12    instantiate variables.*)
    1.13 +local val svc_thy = the_context () in
    1.14 +
    1.15  fun svc_tac i st = 
    1.16 -  let val prem = List.nth (prems_of st, i-1)
    1.17 -      val th = invoke_oracle thy "svc_oracle" 
    1.18 +  let val prem = BasisLibrary.List.nth (prems_of st, i-1)
    1.19 +      val th = invoke_oracle svc_thy "svc_oracle"
    1.20  	             (#sign (rep_thm st), Svc.OracleExn prem)
    1.21     in 
    1.22        compose_tac (false, th, 0) i st
    1.23 @@ -21,6 +23,8 @@
    1.24     handle Svc.OracleExn _ => Seq.empty
    1.25  	| Subscript       => Seq.empty;
    1.26  
    1.27 +end;
    1.28 +
    1.29  
    1.30  (*True if SVC appears to exist*)
    1.31  fun svc_enabled() = getenv "SVC_HOME" <> "";