# HG changeset patch
# User wenzelm
# Date 1139256001 -3600
# Node ID 9000bb9e67187ecec5a386cca34e092d03b8b2b5
# Parent  9881ff995ff573fa17875a944f48af7363b9b296
Logic.combound;

diff -r 9881ff995ff5 -r 9000bb9e6718 src/HOL/ex/SVC_Oracle.ML
--- 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