Logic.combound;

--- a/src/HOL/ex/SVC_Oracle.ML	Mon Feb 06 21:00:00 2006 +0100
+++ b/src/HOL/ex/SVC_Oracle.ML	Mon Feb 06 21:00:01 2006 +0100
@@ -28,8 +28,7 @@
     val pairs = ref ([] : (term*term) list)
     fun insert t =
         let val T = fastype_of t
-            val v = Unify.combound (Var ((!vname,0), Us--->T),
-                                    0, nPar)
+            val v = Logic.combound (Var ((!vname,0), Us--->T), 0, nPar)
         in  vname := Symbol.bump_string (!vname);
             pairs := (t, v) :: !pairs;
             v