src/HOL/Integ/qelim.ML

    |(Const("op |",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_disjI)
    |(Const("op -->",_)$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_impI)
    |(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
               val eth1 = (forall_intr (cterm_of sg (Free(xn1,xT))) th2) COMP  qe_exI
               val th3 = qfnp (snd(qe_get_terms eth1))