src/HOL/Tools/Qelim/cooper.ML

   in case t of
       (l as f $ a) $ b => if skip orelse is_op f then add_bools b o add_bools l
               else insert (op aconv) t
     | f $ a => if skip orelse is_op f then add_bools a o add_bools f
               else insert (op aconv) t
-    | Abs p => add_bools (snd (variant_abs p))
+    | Abs p => add_bools (snd (Syntax_Trans.variant_abs p))  (* FIXME !? *)
     | _ => if skip orelse is_op t then I else insert (op aconv) t
   end;
 
 fun descend vs (abs as (_, xT, _)) =
   let
-    val (xn', p') = variant_abs abs;
+    val (xn', p') = Syntax_Trans.variant_abs abs;  (* FIXME !? *)
   in ((xn', xT) :: vs, p') end;
 
 local structure Proc = Cooper_Procedure in
 
 fun num_of_term vs (Free vT) = Proc.Bound (find_index (fn vT' => vT' = vT) vs)