diff -r 46f5ef758422 -r c9dbce9a23a1 src/HOL/Integ/cooper_dec.ML
--- a/src/HOL/Integ/cooper_dec.ML	Tue Jul 25 21:17:58 2006 +0200
+++ b/src/HOL/Integ/cooper_dec.ML	Tue Jul 25 21:18:00 2006 +0200
@@ -675,7 +675,7 @@
   case fm of 
    Const ("Ex",_) $ Abs(x0,T,p0) => 
    let 
-    val (xn,p1) = variant_abs (x0,T,p0) 
+    val (xn,p1) = Syntax.variant_abs (x0,T,p0) 
     val x = Free (xn,T)  
     val vars = (xn::vars1) 
     val p = unitycoeff x  (posineq (simpl p1))
@@ -694,7 +694,7 @@
 fun cooperpi vars1 fm =
   case fm of
    Const ("Ex",_) $ Abs(x0,T,p0) => let 
-    val (xn,p1) = variant_abs (x0,T,p0)
+    val (xn,p1) = Syntax.variant_abs (x0,T,p0)
     val x = Free (xn,T)
     val vars = (xn::vars1)
     val p = unitycoeff x  (posineq (simpl p1))
@@ -759,7 +759,7 @@
 fun cooper vars1 fm =
   case fm of
    Const ("Ex",_) $ Abs(x0,T,p0) => let 
-    val (xn,p1) = variant_abs (x0,T,p0)
+    val (xn,p1) = Syntax.variant_abs (x0,T,p0)
     val x = Free (xn,T)
     val vars = (xn::vars1)
 (*     val p = unitycoeff x  (posineq (simpl p1)) *)
@@ -794,7 +794,7 @@
 fun cooper_w vars1 fm =
   case fm of
    Const ("Ex",_) $ Abs(x0,T,p0) => let 
-    val (xn,p1) = variant_abs (x0,T,p0)
+    val (xn,p1) = Syntax.variant_abs (x0,T,p0)
     val x = Free (xn,T)
     val vars = (xn::vars1)
 (*     val p = unitycoeff x  (posineq (simpl p1)) *)