1.1 --- a/src/HOL/SVC_Oracle.ML	Tue Aug 03 13:08:18 1999 +0200
     1.2 +++ b/src/HOL/SVC_Oracle.ML	Tue Aug 03 13:08:58 1999 +0200
     1.3 @@ -11,13 +11,14 @@
     1.4  (*Present the entire subgoal to the oracle, assumptions and all, but possibly
     1.5    abstracted.  Use via compose_tac, which performs no lifting but will
     1.6    instantiate variables.*)
     1.7 -val svc_tac = SUBGOAL
     1.8 -  (fn (prem,i) => 
     1.9 -   let val (svc_prem, insts) = Svc.abstract prem
    1.10 -       val th = invoke_oracle thy "svc_oracle" 
    1.11 -	             (sign_of thy, Svc.OracleExn svc_prem)
    1.12 +fun svc_tac i st = 
    1.13 +  let val prem = List.nth (prems_of st, i-1)
    1.14 +      val th = invoke_oracle thy "svc_oracle" 
    1.15 +	             (#sign (rep_thm st), Svc.OracleExn prem)
    1.16 +   in 
    1.17 +      compose_tac (false, th, 0) i st
    1.18 +   end 
    1.19 +   handle Svc.OracleExn _ => Seq.empty
    1.20 +	| Subscript       => Seq.empty;
    1.21  
    1.22 -    in compose_tac (false, th, 0) i
    1.23 -    end handle Svc.OracleExn _ => no_tac);
    1.24  
    1.25 -

     2.1 --- a/src/HOL/SVC_Oracle.thy	Tue Aug 03 13:08:18 1999 +0200
     2.2 +++ b/src/HOL/SVC_Oracle.thy	Tue Aug 03 13:08:58 1999 +0200
     2.3 @@ -9,5 +9,10 @@
     2.4  *)
     2.5  
     2.6  SVC_Oracle = NatBin + (**Real?? + **)
     2.7 +
     2.8 +consts
     2.9 +  (*reserved for the oracle*)
    2.10 +  iff_keep, iff_unfold :: [bool, bool] => bool 
    2.11 +
    2.12  oracle svc_oracle = Svc.oracle
    2.13  end