src/HOL/Tools/meson.ML

 val has_bool_arg_const =
     exists_Const
       (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
 
 (*A higher-order instance of a first-order constant? Example is the definition of
-  HOL.one, 1, at a function type in theory SetsAndFunctions.*)
+  one, 1, at a function type in theory SetsAndFunctions.*)
 fun higher_inst_const thy (c,T) =
   case binder_types T of
       [] => false (*not a function type, OK*)
     | Ts => length (binder_types (Sign.the_const_type thy c)) <> length Ts;