src/HOL/Tools/Sledgehammer/sledgehammer_util.ML

 val is_long_identifier = forall Syntax.is_identifier o space_explode "."
 fun maybe_quote y =
   let val s = unyxml y in
     y |> ((not (is_long_identifier (perhaps (try (unprefix "'")) s)) andalso
            not (is_long_identifier (perhaps (try (unprefix "?")) s))) orelse
-           OuterKeyword.is_keyword s) ? quote
+           Keyword.is_keyword s) ? quote
   end
 
 fun monomorphic_term subst t =
   map_types (map_type_tvar (fn v =>
       case Type.lookup subst v of