src/HOL/Tools/Function/termination.ML

 
     fun mk_compr ineq =
       let
         val (vars, prems, lhs, rhs) = dest_term ineq
       in
-        mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (ObjectLogic.atomize_term thy) prems)
+        mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (Object_Logic.atomize_term thy) prems)
       end
 
     val relation =
       if null ineqs
       then Const (@{const_abbrev Set.empty}, fastype_of rel)