diff -r 2e7d7ec7a268 -r 45a3dc4688bc src/HOL/ex/SVC_Oracle.ML
--- a/src/HOL/ex/SVC_Oracle.ML	Thu Jul 14 19:28:17 2005 +0200
+++ b/src/HOL/ex/SVC_Oracle.ML	Thu Jul 14 19:28:18 2005 +0200
@@ -5,7 +5,7 @@
 
 Installing the oracle for SVC (Stanford Validity Checker)
 
-The following code merely CALLS the oracle; 
+The following code merely CALLS the oracle;
   the soundness-critical functions are at HOL/Tools/svc_funcs.ML
 
 Based upon the work of Søren T. Heilmann
@@ -26,21 +26,21 @@
     val nPar = length params
     val vname = ref "V_a"
     val pairs = ref ([] : (term*term) list)
-    fun insert t = 
-	let val T = fastype_of t
+    fun insert t =
+        let val T = fastype_of t
             val v = Unify.combound (Var ((!vname,0), Us--->T),
-				    0, nPar)
-	in  vname := Symbol.bump_string (!vname); 
-	    pairs := (t, v) :: !pairs;
-	    v
-	end;
-    fun replace t = 
-	case t of
-	    Free _  => t  (*but not existing Vars, lest the names clash*)
-	  | Bound _ => t
-	  | _ => (case gen_assoc Pattern.aeconv (!pairs, t) of
-		      SOME v => v
-		    | NONE   => insert t)
+                                    0, nPar)
+        in  vname := Symbol.bump_string (!vname);
+            pairs := (t, v) :: !pairs;
+            v
+        end;
+    fun replace t =
+        case t of
+            Free _  => t  (*but not existing Vars, lest the names clash*)
+          | Bound _ => t
+          | _ => (case gen_assoc Pattern.aeconv (!pairs, t) of
+                      SOME v => v
+                    | NONE   => insert t)
     (*abstraction of a numeric literal*)
     fun lit (t as Const("0", _)) = t
       | lit (t as Const("1", _)) = t
@@ -66,11 +66,11 @@
       | nat t = lit t
     (*abstraction of a relation: =, <, <=*)
     fun rel (T, c $ x $ y) =
-	    if T = HOLogic.realT then c $ (rat x) $ (rat y)
-	    else if T = HOLogic.intT then c $ (int x) $ (int y)
-	    else if T = HOLogic.natT then c $ (nat x) $ (nat y)
-	    else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
-	    else replace (c $ x $ y)   (*non-numeric comparison*)
+            if T = HOLogic.realT then c $ (rat x) $ (rat y)
+            else if T = HOLogic.intT then c $ (int x) $ (int y)
+            else if T = HOLogic.natT then c $ (nat x) $ (nat y)
+            else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
+            else replace (c $ x $ y)   (*non-numeric comparison*)
     (*abstraction of a formula*)
     and fm ((c as Const("op &", _)) $ p $ q) = c $ (fm p) $ (fm q)
       | fm ((c as Const("op |", _)) $ p $ q) = c $ (fm p) $ (fm q)
@@ -92,20 +92,13 @@
 (*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 = BasisLibrary.List.nth (prems_of st, i-1)
-      val (absPrem, _) = svc_abstract prem
-      val th = invoke_oracle svc_thy "svc_oracle"
-	             (#sign (rep_thm st), Svc.OracleExn absPrem)
-   in 
-      compose_tac (false, th, 0) i st
-   end 
-   handle Svc.OracleExn _ => Seq.empty
-	| Subscript       => Seq.empty;
-
-end;
+fun svc_tac i st =
+  let
+    val (abs_goal, _) = svc_abstract (Logic.get_goal (Thm.prop_of st) i)
+    val th = svc_oracle (Thm.theory_of_thm st) abs_goal
+   in compose_tac (false, th, 0) i end
+   handle TERM _ => no_tac;
 
 
 (*check if user has SVC installed*)