src/HOL/Import/shuffler.ML

   | swap_bound n (Abs(x,xT,t)) = Abs(x,xT,swap_bound (n+1) t)
   | swap_bound n t = t
 
 fun rew_th thy (xv as (x,xT)) (yv as (y,yT)) t =
     let
-        val lhs = list_all ([xv,yv],t)
-        val rhs = list_all ([yv,xv],swap_bound 0 t)
+        val lhs = Logic.list_all ([xv,yv],t)
+        val rhs = Logic.list_all ([yv,xv],swap_bound 0 t)
         val rew = Logic.mk_equals (lhs,rhs)
         val init = Thm.trivial (cterm_of thy rew)
     in
         all_comm RS init
     end