src/HOL/ex/SVC_Oracle.ML

     val nPar = length params
     val vname = ref "V_a"
     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
         end;
     fun replace t =