--- a/src/HOL/Tools/Presburger/qelim.ML Tue Jul 25 21:17:58 2006 +0200
+++ b/src/HOL/Tools/Presburger/qelim.ML Tue Jul 25 21:18:00 2006 +0200
@@ -40,7 +40,7 @@
|(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
|(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not)
|(Const("Ex",_)$Abs(xn,xT,p)) =>
- let val (xn1,p1) = variant_abs(xn,xT,p)
+ let val (xn1,p1) = Syntax.variant_abs(xn,xT,p)
in ([p1],
fn [th1_1] =>
let val th2 = [th1_1,nfnp (snd (qe_get_terms th1_1))] MRS trans